English
For any continuous map f: X → Σ i, Y_i with X connected, there exists i and g: X → Y_i such that f = sigmaMk i ∘ g.
Русский
Для произвольной непрерывной карты f: X → Σ_i Y_i с объединённым пространством X, существует индекс i и карта g: X → Y_i такая, что f = σMk i ∘ g.
LaTeX
$$$\\exists i\\; \\exists g\\; f = (\\sigmaMk i).comp g$$$
Lean4
/-- Every continuous map from a connected topological space to the disjoint union of a family of
topological spaces is a composition of the embedding `ContinuousMap.sigmaMk i : C(Y i, Σ i, Y i)`
for some `i` and a continuous map `g : C(X, Y i)`. See also `Continuous.exists_lift_sigma` for a
version with unbundled functions and `ContinuousMap.sigmaCodHomeomorph` for a homeomorphism defined
using this fact. -/
theorem exists_lift_sigma (f : C(X, Σ i, Y i)) : ∃ i g, f = (sigmaMk i).comp g :=
let ⟨i, g, hg, hfg⟩ := (map_continuous f).exists_lift_sigma
⟨i, ⟨g, hg⟩, DFunLike.ext' hfg⟩
