piMap — Mathlib

English

The map that applies coordinatewise isometry on each factor induces an isometry on the Pi-space.

Русский

Координатно-изометрическое отображение на каждом факторе порождает изометрическую карту на пространстве Pi.

LaTeX

$$$Isometry\\ (Pi.map f) = (\\forall i, Isometry (f_i)) \\\\Rightarrow Isometry (Pi.map f))$$$

Lean4

protected theorem piMap {ι} [Fintype ι] {α β : ι → Type*} [∀ i, PseudoEMetricSpace (α i)]
    [∀ i, PseudoEMetricSpace (β i)] (f : ∀ i, α i → β i) (hf : ∀ i, Isometry (f i)) : Isometry (Pi.map f) := fun x y =>
  by simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]

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