edist_one_right — Mathlib

English

In a normed group, the distance from a to the multiplicative unit 1 equals the EN-norm of a: edist(a,1) = ‖a‖ₑ.

Русский

В нормированой группе расстояние от элемента a до единицы 1 равно EN-норме элемента a: edist(a,1) = ‖a‖ₑ.

LaTeX

$$$\mathrm{edist}(a,1) = \|a\|_{\varepsilon}.$$$

Lean4

@[to_additive (attr := simp)]
theorem edist_one_right (a : E) : edist a 1 = ‖a‖ₑ := by simp [edist_nndist, nndist_one_right, enorm]

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