dist_vadd_right

Mathlib.Analysis.Normed.Group.AddTorsor

URI: https://scilib.ai/kg/mathlib#dist_vadd_right

English

The distance between x and v +ᵥ x equals the norm of v.

Русский

Расстояние между x и v +ᵥ x равно норме вектора v.

LaTeX

$$dist x (v +ᵥ x) = ‖v‖$$

Lean4

@[simp]
theorem dist_vadd_right (v : V) (x : P) : dist x (v +ᵥ x) = ‖v‖ := by rw [dist_comm, dist_vadd_left]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru