Gleason — Mathlib

English

A compact Hausdorff space X is projective in CompHaus iff X is extremally disconnected.

Русский

Компактное хаусдорфово пространство X проективно в CompHaus тогда и только тогда, когда оно экстремально разобщено.

LaTeX

$$$\mathrm{Projective}(X) \iff \operatorname{ExtremallyDisconnected}(X)$$$

Lean4

theorem Gleason (X : CompHaus.{u}) : Projective X ↔ ExtremallyDisconnected X :=
  by
  constructor
  · intro h
    change ExtremallyDisconnected X.toStonean
    infer_instance
  · intro h
    let X' : Stonean := ⟨X.toTop, inferInstance⟩
    change Projective X'.compHaus
    apply Stonean.instProjectiveCompHausCompHaus

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