English
Let X be a type and l a filter on X. The map x ↦ pure x (the principal filter generated by x) is continuous from X to the space of filters on X with its natural topology; equivalently, for every l, Tendsto (pure : X → Filter X) l (𝓝 l).
Русский
Пусть X — множество и l — фильтр на X. Отображение x ↦ принципиальный фильтр {x} (порожденный фильтр) непрерывно отображает X в пространство фильтров на X, то есть для каждого l выполняется Tendsto (pure) l (𝓝 l).
LaTeX
$$$\forall X, \forall l : \text{Filter}(X),\; \mathrm{Tendsto}(\mathrm{pure} : X \to \text{Filter}(X))\, l\, 𝓝 l$$$
Lean4
protected theorem tendsto_pure_self (l : Filter X) : Tendsto (pure : X → Filter X) l (𝓝 l) :=
by
rw [Filter.tendsto_nhds]
exact fun s hs ↦ Eventually.mono hs fun x ↦ id
