to_isIsIsometricVAdd — Mathlib

English

The action of V on P in a NormedAddTorsor is isometric; translating an element v ∈ V by any points x, y in P preserves distances.

Русский

Действие V на P в NormedAddTorsor изометрично; сдвиги на одинаковый v сохраняют расстояния между точками.

LaTeX

$$IsIsometricVAdd(V, P) holds: расстояние не изменяется под переносом$$

Lean4

instance (priority := 100) to_isIsIsometricVAdd : IsIsometricVAdd V P :=
  ⟨fun c => Isometry.of_dist_eq fun x y => by simp [NormedAddTorsor.dist_eq_norm']⟩

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