instFunLike — Mathlib

English

The type of coalgebra equivalences A ≃ₗc[R] B is equipped with EquivLike structure, enabling function-like behavior and equality via underlying maps.

Русский

Тип коалгебраических эквивалентностей A ≃ₗc[R] B снабжен структурой EquivLike, позволяющей вести себя как множество биекций и определять равенство через подлежащие отображения.

LaTeX

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

Lean4

instance : FunLike (A ≃ₗc[R] B) A B where
  coe := DFunLike.coe
  coe_injective' := DFunLike.coe_injective

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