English
If f is bijective and each g_i is a homeomorphism, then Sigma.map f g is a homeomorphism.
Русский
Если f — биективно и каждый g_i — гомеоморфизм, то Sigma.map f g — гомеоморфизм.
LaTeX
$$$\text{Bijective}(f) \to \forall i, \IsHomeomorph(g_i) \to \IsHomeomorph(\Sigma.map f g)$$$
Lean4
theorem sigmaMap {ι κ : Type*} {X : ι → Type*} {Y : κ → Type*} [∀ i, TopologicalSpace (X i)]
[∀ i, TopologicalSpace (Y i)] {f : ι → κ} (hf : Bijective f) {g : (i : ι) → X i → Y (f i)}
(hg : ∀ i, IsHomeomorph (g i)) : IsHomeomorph (Sigma.map f g) :=
by
simp_rw [isHomeomorph_iff_isEmbedding_surjective, ] at hg ⊢
exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩
