mapClusterPt_iff_ultrafilter — Mathlib

English

A map cluster point relation maps s to x through an ultrafilter on the index set: MapClusterPt x F u is equivalent to the existence of an ultrafilter U ≤ F with Tendsto(u, U, 𝓝 x).

Русский

Отображение кластерной точки задаётся через ультрафильтр на индексном множестве: MapClusterPt x F u ⇔ существует ультрафильтр U ≤ F с Tendsto(u, U, 𝓝 x).

LaTeX

$$$MapClusterPt(x, F, u) \\iff \\exists U : Ultrafilter α, U \\le F \\land Tendsto(u, U, 𝓝 x)$$$

Lean4

theorem mapClusterPt_iff_ultrafilter : MapClusterPt x F u ↔ ∃ U : Ultrafilter α, U ≤ F ∧ Tendsto u U (𝓝 x) := by
  simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap, ← le_inf_iff,
    exists_ultrafilter_iff, inf_comm]

Похожие утверждения