star_isometry — Mathlib

English

In a normed star group, the star map is an isometry: ||star x − star y|| = ||x − y|| for all x,y.

Русский

В нормированной звёздной группе отображение звезды является изометрией: для всех x,y выполняется ||x⋆ − y⋆|| = ||x − y||.

LaTeX

$$Isometry (star : E → E):= ∀ x,y, \|x^{\star} - y^{\star}\| = \|x - y\|$$

Lean4

/-- The `star` map in a normed star group is an isometry -/
theorem star_isometry : Isometry (star : E → E) :=
  show Isometry starAddEquiv from AddMonoidHomClass.isometry_of_norm starAddEquiv (show ∀ x, ‖x⋆‖ = ‖x‖ from norm_star)

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