dist_map — Mathlib

English

Alternatively to norm preservation for linear maps, ∥f(x)∥ = ∥x∥ for all x.

Русский

Альтернативно сохранение нормы линейного отображения: для всех x выполняется ∥f(x)∥ = ∥x∥.

LaTeX

$$$\forall x,\ \|f(x)\| = \|x\|$$$

Lean4

@[simp]
theorem dist_map (x y : P) : dist (f x) (f y) = dist x y := by
  rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]

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