prodMap — Mathlib

English

The product map of two isometries is an isometry on the product space.

Русский

Произведение отображений, сохраняющих расстояния, также изометрично на произведении пространств.

LaTeX

$$$Isometry\\ (Prod.map f g) = (Isometry f) \\land (Isometry g)$$$

Lean4

theorem prodMap {δ} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf : Isometry f) (hg : Isometry g) :
    Isometry (Prod.map f g) := fun x y => by
  simp only [Prod.edist_eq, Prod.map_fst, hf.edist_eq, Prod.map_snd, hg.edist_eq]

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