English
If X is compact Hausdorff and projective, then X is extremally disconnected.
Русский
Если X компактно-гладко (компактно-хаусдорфово) и проективно, то X является экстремально разобщим.
LaTeX
$$$$ \\text{If } X \\text{ is compact Hausdorff and projective, then } ExtremallyDisconnected X. $$$$
Lean4
/-- Lemma 2.3 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection from a compact Hausdorff space to an extremally disconnected Hausdorff space
satisfying the "Zorn subset condition" is a homeomorphism. -/
noncomputable def homeoCompactToT2 [ExtremallyDisconnected A] [T2Space A] [T2Space E] [CompactSpace E] {ρ : E → A}
(ρ_cont : Continuous ρ) (ρ_surj : ρ.Surjective)
(zorn_subset : ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ) : E ≃ₜ A :=
ρ_cont.homeoOfEquivCompactToT2 (f :=
Equiv.ofBijective ρ ⟨homeoCompactToT2_injective ρ_cont ρ_surj zorn_subset, ρ_surj⟩)
