instCoeToCoalgEquiv — Mathlib

English

There is a canonical coercion from any F with EquivLike and CoalgEquivClass to a coalgebra equivalence, defined by coe f := toCoalgEquiv f.

Русский

Существует каноническое приведение типа из F в коалгебра эквалент через конструктор toCoalgEquiv; определение via coe f = toCoalgEquiv f.

LaTeX

$$$\text{coe} : F \to (A \equiv_{\text{coalgebra}} B)$ is defined by $\mathrm{coe}(f) = \mathrm{toCoalgEquiv}(f)$.$$

Lean4

/-- Reinterpret an element of a type of coalgebra equivalences as a coalgebra equivalence. -/
instance instCoeToCoalgEquiv [EquivLike F A B] [CoalgEquivClass F R A B] : CoeHead F (A ≃ₗc[R] B) where
  coe f := toCoalgEquiv f

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