Theorems · Theorem · general topology

exists_compact_surjective_zorn_subset

∀ {A D : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace D] [T1Space A] [CompactSpace D] {X : D → A},
  Continuous X →
    Function.Surjective X →
      ∃ E,
        CompactSpace ↑E ∧
          X '' E = Set.univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ Set.univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ Set.univ

Lemma 2.4 in [Gleason, Projective topological spaces][gleason1958]: a continuous surjection $\pi$ from a compact space $D$ to a Fréchet space $A$ restricts to a compact subset $E$ of $D$, such that $\pi$ maps $E$ onto $A$ and satisfies the "Zorn subset condition", where $\pi(E_0) \ne A$ for any proper closed subset $E_0 \subsetneq E$.

Defined in

Mathlib.Topology.ExtremallyDisconnected

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT1SpaceCompactSpace