ultrafilter_extend_extends — Mathlib

English

If g is continuous, and F,G are ultrafilters on α with x a common limit, then extending g along F and G yields the same value.

Русский

Если g непрерывна и F,G — ультрафильтры над α с общим пределом x, то они имеют одинаковое значение после применения Ultrafilter.extend.

LaTeX

$$$Ultrafilter\.extend\ g\ F = Ultrafilter\.extend\ g\ G$$$

Lean4

@[simp]
theorem ultrafilter_extend_extends (f : α → γ) : Ultrafilter.extend f ∘ pure = f :=
  by
  letI : TopologicalSpace α := ⊥
  haveI : DiscreteTopology α := ⟨rfl⟩
  exact funext (isDenseInducing_pure.extend_eq continuous_of_discreteTopology)

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