Theorems · Definition · general topology

CompactT2.Projective

(X : Type u) → [TopologicalSpace X] → Prop

The assertion CompactT2.Projective states that given continuous maps f : X → Z and g : Y → Z with g surjective between t_2, compact topological spaces, there exists a continuous lift h : X → Y, such that f = g ∘ h.

Defined in

Mathlib.Topology.ExtremallyDisconnected

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpace