English
For every ultrafilter u on Ultrafilter α and every x in Ultrafilter α, u converges to x if and only if x equals joinM u (the ultrafilter limit of u).
Русский
Пусть u — ультрафильтр на Ultrafilter α, и x — элемент Ultrafilter α. Тогда u сходится к x тогда и только тогда, когда x = joinM u.
LaTeX
$$$(\uparrow u \le 𝓝 x) \iff x = \mathrm{joinM}\,u$$$
Lean4
/-- Every ultrafilter `u` on `Ultrafilter α` converges to a unique
point of `Ultrafilter α`, namely `joinM u`. -/
theorem ultrafilter_converges_iff {u : Ultrafilter (Ultrafilter α)} {x : Ultrafilter α} : ↑u ≤ 𝓝 x ↔ x = joinM u :=
by
rw [eq_comm, ← Ultrafilter.coe_le_coe]
change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff, mem_setOf_eq]
constructor
· intro h a ha
exact h _ ⟨ha, a, rfl⟩
· rintro h a ⟨xi, a, rfl⟩
exact h _ xi
