continuous_ultrafilter_extend — Mathlib

English

Reiteration: Ultrafilter.extend f is continuous when γ is compact Hausdorff, for any f: α → γ.

Русский

Повторение: Ultrafilter.extend f непрерывно для компактного хаусдорфово γ; f: α → γ.

LaTeX

$$$Continuous\big(Ultrafilter\.extend\ f\big)$$$

Lean4

theorem continuous_ultrafilter_extend (f : α → γ) : Continuous (Ultrafilter.extend f) :=
  by
  have h (b : Ultrafilter α) : ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
    -- b.map f is an ultrafilter on γ, which is compact, so it converges to some c in γ.
    let ⟨c, _, h'⟩ := isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem)
    ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩
  let _ : TopologicalSpace α := ⊥
  exact isDenseInducing_pure.continuous_extend h

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