instGroup — Mathlib

English

Affine isometries preserve the distance between any two points: dist(e x, e y) = dist(x, y).

Русский

Аффинные изометрии сохраняют расстояние между произвольными двумя точками: dist(e x, e y) = dist(x, y).

LaTeX

$$$\mathrm{dist}(e(x), e(y)) = \mathrm{dist}(x, y)$$$

Lean4

/-- The group of affine isometries of a `NormedAddTorsor`, `P`. -/
instance instGroup : Group (P ≃ᵃⁱ[𝕜] P) where
  mul e₁ e₂ := e₂.trans e₁
  one := refl _ _
  inv := symm
  one_mul := trans_refl
  mul_one := refl_trans
  mul_assoc _ _ _ := trans_assoc _ _ _
  inv_mul_cancel := self_trans_symm

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