Theorems · Theorem · general topology

CompactT2.ExtremallyDisconnected.projective

∀ {A : Type u} [inst : TopologicalSpace A] [ExtremallyDisconnected A] [CompactSpace A] [T2Space A],
  CompactT2.Projective A

Theorem 2.5 in [Gleason, Projective topological spaces][gleason1958]: in the category of compact spaces and continuous maps, the projective spaces are precisely the extremally disconnected spaces.

Defined in

Mathlib.Topology.ExtremallyDisconnected

Cited by

1 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceExtremallyDisconnectedCompactSpaceT2Space