Theorems · Theorem · general topology

ContinuousMap.exists_lift_sigma

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

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.

Defined in

Mathlib.Topology.ContinuousMap.Sigma

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceConnectedSpace