instGroup — Mathlib

English

The map taking a Homeomorph inverse applied to a symmetric structure equals the symmetric inverse of the original Homeomorph.

Русский

Обратное к гомеоморфизму через симм сохраняет симметрию исходной структуры.

LaTeX

$$$ (e.toHomeomorph)^{-1} = e.symm $$$

Lean4

instance instGroup : Group (E ≃ₗᵢ[R] E) 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

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