The most obvious way that a function can move a set around is via the image construction. The function gives us some kind of dynamics in the system - we can start using the function to move sets around. Let’s stick with “usual” subsets for this section, but let’s throw in a second type Y and a function f : X → Y. In reality these filters are defined completely rigorously as some collection of usual subsets satisfying some axioms but we won’t go into these this week, we’ll just stick with the picture. Just like usual subsets, these generalised subsets have a partial order, which we’ll call, extending the partial order on usual subsets. For example, if X = ℝ then there’s a filter called 𝓝 0, the neighbourhood filter of 0, which should be thought of as containing 0 and all the infinitesimally small numbers. Each subset S of X gives you a filter, called the principal filter 𝓟 S, and there are other filters too corresponding to slightly weirder things. However it was equally clear that infinitesimals provided a good picture.Ī filter on X is a kind of “generalised subset” of X. By the 20th century, the experts had made their decision: there were no infinitesimally small nonzero real numbers, and that’s what the textbooks say today (other than Robinson’s book on non-standard analysis, but nobody uses that for teaching undergraduate calculus). However, people had not quite worked out whether infinitesimals existed - infinitely small non-zero real numbers called things like and - and some people like Leibniz wanted to divide one of them by the other because they were discovering some new-fangled thing called calculus. Back in the days of Isaac Newton, one particularly well-studied type was the type of real numbers. The type of subsets of X has a bunch of nice structure - there’s a partial order, there are unions and intersections (both finite and infinite) and they satisfy a bunch of axioms. Let X be a type (you can call it a set if you like). Reminder: filters are generalised subsets So this week I’m going to talk about tendsto, but first I think it’s worth refreshing our memories about the useful mental picture of a filter as a generalised subset. I talked about limits of sequences of real numbers in workshop 3, but this week I come back to them, because this week we’ll see that the usual ten-line proof that if and then can be replaced by a two-line proof involving something called filter.tendsto_mul.

Math infinitesimals are nonsense