nndist_one_left — Mathlib

English

For any element a in a seminormed group E, the nonnegative distance between 1 and a equals the NN-norm of a: nndist 1 a = ‖a‖₊.

Русский

Для любого a в полугруппе с нормой расстояние от 1 до a равно NN-норме a: nndist(1, a) = ‖a‖₊.

LaTeX

$$$$ \\operatorname{nndist}(1, a) = \\|a\\|_{+} $$$$

Lean4

@[to_additive (attr := simp)]
theorem nndist_one_left (a : E) : nndist 1 a = ‖a‖₊ := by simp [nndist_eq_nnnorm_div]

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