isometry_extend — Mathlib

English

The extension operator with fixed f and h acts as an isometry on g.

Русский

Оператор расширения с фиксированными f и h действует как изометрия на g.

LaTeX

$$$\\text{Isometry}(\\lambda g:\\alpha \\to^\\mathrm{b} \\beta \\mapsto \\text{extend}(f,g,h))$$$

Lean4

theorem isometry_extend (f : α ↪ δ) (h : δ →ᵇ β) : Isometry fun g : α →ᵇ β => extend f g h :=
  Isometry.of_dist_eq fun g₁ g₂ => by simp

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