nndist_toAdd — Mathlib

English

Symmetric preservation of distance by toAdd between Multiplicative elements and their Additive counterparts.

Русский

Сохранение расстояния отображением toAdd между мультипликативными элементами и их аддитивными аналогами.

LaTeX

$$$\operatorname{nndist}(a^{\mathrm{toAdd}}, b^{\mathrm{toAdd}}) = \operatorname{nndist}(a,b)$$$

Lean4

@[simp]
theorem nndist_toAdd (a b : Multiplicative X) : nndist a.toAdd b.toAdd = nndist a b :=
  rfl

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