English
For a discrete space X, the Stone–Čech compactification StoneCech X is projective in the CompactT2 sense.
Русский
Для дискретного пространства X кампания Stone–Čech X является проективной в смысле CompactT2.
LaTeX
$$$$ \\text{Discrete}(X) \\Rightarrow \\text{CompactT2.Projective}(\\text{StoneCech }X). $$$$
Lean4
/-- 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`. -/
def Projective : Prop :=
∀ {Y Z : Type u} [TopologicalSpace Y] [TopologicalSpace Z],
∀ [CompactSpace Y] [T2Space Y] [CompactSpace Z] [T2Space Z],
∀ {f : X → Z} {g : Y → Z} (_ : Continuous f) (_ : Continuous g) (_ : Surjective g),
∃ h : X → Y, Continuous h ∧ g ∘ h = f
