isometry_of_comp — Mathlib

English

If the absolute value v factors through an embedding f into a normed field L, and ∥f x∥ = v x for all x, then f is an isometry.

Русский

Если величина v фактизирует отображение через вложение f в нормированное поле L и для всех x выполняется ∥f x∥ = v x, то f является изометрией.

LaTeX

$$$$\\forall x,\\; \\|f(x)\\| = v(x) \\;\Rightarrow\\; f \\text{ is an isometry}.$$$$

Lean4

/-- If the absolute value `v` factors through an embedding `f` into a normed field, then
`f` is an isometry. -/
theorem isometry_of_comp (h : ∀ x, ‖f x‖ = v x) : Isometry f :=
  Isometry.of_dist_eq <| fun x y => by simp only [‹NormedField L›.dist_eq, ← f.map_sub, h]; rfl

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