instEquivLike — Mathlib

English

There is an EquivLike structure on the family of equivalences between group extensions, relating E and E'.

Русский

Существует структура EquivLike над семейством эквивалентностей между вложениями групп, связывающая E и E'.

LaTeX

$$$\\mathrm{EquivLike}(S.\\mathrm{Equiv} S')\\ E\\ E'$$$

Lean4

@[to_additive]
instance : EquivLike (S.Equiv S') E E' where
  coe equiv := equiv.toMulEquiv
  inv equiv := equiv.toMulEquiv.symm
  left_inv equiv := equiv.left_inv
  right_inv equiv := equiv.right_inv
  coe_injective' := fun ⟨_, _, _⟩ ⟨_, _, _⟩ h _ ↦ by
    congr
    rw [MulEquiv.ext_iff]
    exact congrFun h

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