nndist_vadd_cancel_right

Mathlib.Analysis.Normed.Group.AddTorsor

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

← MathLib Explorer

English

Similarly, the equality holds at the level of the underlying distance (nnreal).

Русский

Аналогично, равенство сохраняется на уровне соответствующего расстояния.

LaTeX

$$nndist (v +ᵥ x) (v +ᵥ y) = nndist x y$$

Lean4

@[simp]
theorem nndist_vadd_cancel_right (v₁ v₂ : V) (x : P) : nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂ :=
  NNReal.eq <| dist_vadd_cancel_right _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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