isometry_iff_norm — Mathlib

English

For a homomorphism f between seminormed groups, f is an isometry if and only if ∥f x∥ = ∥x∥ for all x.

Русский

Для гомоморфизма f между полугруппами с нормами выполняется: f является изометрией тогда и только тогда, когда для всех x выполняется ∥f x∥ = ∥x∥.

LaTeX

$$$\mathrm{Isometry}(f) \iff \forall x,\ \|f x\| = \|x\|.$$$

Lean4

@[to_additive]
theorem isometry_iff_norm [MonoidHomClass 𝓕 E F] (f : 𝓕) : Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖ :=
  by
  simp only [isometry_iff_dist_eq, dist_eq_norm_div, ← map_div]
  refine ⟨fun h x => ?_, fun h x y => h _⟩
  simpa using h x 1

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