extend — Mathlib

English

If γ is a compact Hausdorff space, then Ultrafilter.extend f is continuous for any f: α → γ.

Русский

Пусть γ — компактно-хаусдорфово пространство. Тогда Ultrafilter.extend f непрерывно для любого f: α → γ.

LaTeX

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

Lean4

/-- The extension of a function `α → γ` to a function `Ultrafilter α → γ`.
  When `γ` is a compact Hausdorff space it will be continuous. -/
def extend (f : α → γ) : Ultrafilter α → γ :=
  letI : TopologicalSpace α := ⊥
  isDenseInducing_pure.extend f

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