continuous_preStoneCechUnit — Mathlib

English

preStoneCechUnit x is the equivalence class of pure x in PreStoneCech α.

Русский

preStoneCechUnit x — эквивалентный класс чистого x в PreStoneCech α.

LaTeX

$$preStoneCechUnit\ x = Quot.mk\_\big(\lambda F\ G, \; ∃ z, F ≤ 𝓝 z ∧ G ≤ 𝓝 z\big) (\mathrm{pure}(x))$$

Lean4

theorem continuous_preStoneCechUnit : Continuous (preStoneCechUnit : α → PreStoneCech α) :=
  continuous_iff_ultrafilter.mpr fun x g gx ↦
    by
    have : (g.map pure).toFilter ≤ 𝓝 g :=
      by
      rw [ultrafilter_converges_iff, ← bind_pure g]
      rfl
    have : (map preStoneCechUnit g : Filter (PreStoneCech α)) ≤ 𝓝 (Quot.mk _ g) :=
      (map_mono this).trans (continuous_quot_mk.tendsto _)
    convert this
    exact Quot.sound ⟨x, pure_le_nhds x, gx⟩

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