isProperMap_iff_ultrafilter_of_t2

English

In a T2 space setting, the same ultrafilter characterization simplifies to using 𝒰.1 ≤ nhds x.

Русский

В пространстве T2 характеризация ультрафильтров упрощается до условия 𝒰.1 ≤ nhds x.

LaTeX

$$$IsProperMap(f) \iff (Continuous(f) \land ∀ 𝒰\!:\!Ultrafilter X, ∀ y, Tendsto f 𝒰 (nhds y) \rightarrow ∃ x, 𝒰.1 ≤ nhds x)$$$

Lean4

theorem isProperMap_iff_ultrafilter_of_t2 [T2Space Y] :
    IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄, ∀ ⦃y : Y⦄, Tendsto f 𝒰 (𝓝 y) → ∃ x, 𝒰.1 ≤ 𝓝 x :=
  isProperMap_iff_ultrafilter.trans <|
    and_congr_right fun hc ↦
      forall₃_congr fun _𝒰 _y hy ↦
        exists_congr fun x ↦ and_iff_right_of_imp fun h ↦ tendsto_nhds_unique ((hc.tendsto x).mono_left h) hy

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