pi_map — Mathlib

English

If all f_i are homeomorphisms, then the map (x_i) ↦ (f_i(x_i)) is a homeomorphism.

Русский

Если все f_i — гомеоморфизмы, то отображение (x_i) ↦ (f_i(x_i)) является гомеоморфизмом.

LaTeX

$$$\forall i, \IsHomeomorph(f_i) \Rightarrow \IsHomeomorph(\lambda x, f_i(x_i))$$$

Lean4

theorem pi_map {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)]
    {f : (i : ι) → X i → Y i} (h : ∀ i, IsHomeomorph (f i)) : IsHomeomorph (fun (x : ∀ i, X i) i ↦ f i (x i)) :=
  (Homeomorph.piCongrRight fun i ↦ (h i).homeomorph (f i)).isHomeomorph

Похожие утверждения