instEquivLike — Mathlib

English

The family of coalgebra equivalences A ≃ₗc[R] B carries a natural EquivLike structure, so elements act as bijective maps A → B with coherent inverses.

Русский

Семейство коалгебраических эквивалентностей A ≃ₗc[R] B имеет естественную структуру EquivLike, то что элементы ведут как биекции A → B с согласованными обратными.

LaTeX

$$$\\operatorname{EquivLike}(A \\simeq_{\\ell_c[R]} B)\\; A\\; B$$$

Lean4

instance : EquivLike (A ≃ₗc[R] B) A B where
  coe e := e.toFun
  inv := CoalgEquiv.invFun
  coe_injective' _ _ h _ := toCoalgHom_injective (DFunLike.coe_injective h)
  left_inv := CoalgEquiv.left_inv
  right_inv := CoalgEquiv.right_inv

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