English
There is a homeomorphism between the space C(X, Σ_i Y_i) and the sigma-product of the C(X, Y_i), given by sigmaCodHomeomorph, with inverse sending (i,g) to (σMk i) ∘ g.
Русский
Существует гомеоморфизм между пространством C(X, Σ_i Y_i) и суммарной схемой C(X, Y_i), задаваемый sigmaCodHomeomorph, чей обратный образ отправляет (i,g) в (σMk i) ∘ g.
LaTeX
$$$C(X,\\Sigma i\,Y_i) \\cong_t \\Sigma i\\; C(X,Y_i)$$$
Lean4
/-- 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`. -/
@[simps! symm_apply]
def sigmaCodHomeomorph : C(X, Σ i, Y i) ≃ₜ Σ i, C(X, Y i) :=
.symm <|
Equiv.toHomeomorphOfIsInducing
(.ofBijective _
⟨isEmbedding_sigmaMk_comp.injective, fun f ↦
let ⟨i, g, hg⟩ := f.exists_lift_sigma;
⟨⟨i, g⟩, hg.symm⟩⟩)
isEmbedding_sigmaMk_comp.isInducing
