coe_coe — Mathlib

English

For any coalgebra homomorphism f, its action as a function coincides with the map f itself; i.e., viewing f as a function A → B gives the same map as f

Русский

Для любого координатного гомоморфизма коалграбра A → B его действие как отображения совпадает с самим гомоморфизмом; то есть при рассмотрении f как функции A → B получаем тот же отображение

LaTeX

$$$$ (f : A \to B) = f $$$$

Lean4

@[simp]
protected theorem coe_coe {F : Type*} [FunLike F A B] [CoalgHomClass F R A B] (f : F) : ⇑(f : A →ₗc[R] B) = f :=
  rfl

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