ContinuousMap.exists_lift_sigma

theorem ContinuousMap.exists_lift_sigma : ∀ {X : Type u_1} {ι : Type u_2} {Y : ι → Type u_3} [inst : TopologicalSpace X] [inst_1 : (i : ι) → TopologicalSpace (Y i)] [inst_2 : ConnectedSpace X] (f : C(X, (i : ι) × Y i)), ∃ i g, f = (ContinuousMap.sigmaMk i).comp g

This theorem states that for any continuous map from a connected topological space to the disjoint union of a family of topological spaces, there exists an index `i` and a continuous map `g` such that the original map `f` can be composed from `g` and the embedding `ContinuousMap.sigmaMk i : C(Y i, Σ i, Y i)`. Essentially, any such map `f` can be decomposed into these two parts: an embedding associated with a particular index `i`, and a continuous map `g`. This theorem is used in the definition of a homeomorphism `ContinuousMap.sigmaCodHomeomorph` and also has an unbundled version `Continuous.exists_lift_sigma`.

More concisely: Given any continuous function from a connected topological space to the disjoint union of a family of topological spaces, there exists an index `i` and a continuous map such that the original function can be expressed as the composition of the map with the embedding of the indexed space.