dist_one — Mathlib

English

In a seminormed group, the distance from the identity element to any element x equals the norm of x: dist(1, x) = ||x|| for every x in E.

Русский

В полугруппе с нормой расстояние от единицы до любого элемента x равно норме элемента: dist(1, x) = ||x|| для всех x ∈ E.

LaTeX

$$$\forall x\in E\, \operatorname{dist}(1, x) = \|x\|$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_one : dist (1 : E) = norm :=
  funext dist_one_left

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