projective_iff_extremallyDisconnected

English

For a compact Hausdorff space A, Projective A is equivalent to ExtremallyDisconnected A.

Русский

Для компактного хаусдорфового пространства A проективность A эквивалентна его экстремальной разобщенности.

LaTeX

$$$$ [CompactSpace A] \\land [T2Space A] \\Rightarrow (CompactT2.Projective A) \\iff (ExtremallyDisconnected A). $$$$

Lean4

protected theorem projective_iff_extremallyDisconnected [CompactSpace A] [T2Space A] :
    Projective A ↔ ExtremallyDisconnected A :=
  ⟨Projective.extremallyDisconnected, fun _ => ExtremallyDisconnected.projective⟩

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