Theorems · Definition · general topology

ContinuousMap.sigmaCodHomeomorph

(X : Type u_1) →
  {ι : Type u_2} →
    (Y : ι → Type u_3) →
      [inst : TopologicalSpace X] →
        [inst_1 : (i : ι) → TopologicalSpace (Y i)] → [ConnectedSpace X] → C(X, (i : ι) × Y i) ≃ₜ (i : ι) × C(X, Y i)

Homeomorphism between the type C(X, Σ i, Y i) of continuous maps from a connected topological space to the disjoint union of a family of topological spaces and the disjoint union of the types of continuous maps C(X, Y i). The inverse map sends ⟨i, g⟩ to ContinuousMap.comp (ContinuousMap.sigmaMk i) g.

Defined in

Mathlib.Topology.ContinuousMap.Sigma

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceConnectedSpace