coe_fn_inj — Mathlib

English

The map from coalgebra homs to their underlying linear maps is injective: equal linear maps imply equal coalgebra homs

Русский

Картирование коалгоморфизмов в соответствующие линейные отображения инъективно: равные линейные отображения определяют одинаковые коалгоморфизмы

LaTeX

$$$$ (\phi_1 = \phi_2) \Rightarrow (\phi_1^{\mathrm{toLinearMap}} = \phi_2^{\mathrm{toLinearMap}}) $$$$

Lean4

theorem coe_fn_inj {φ₁ φ₂ : A →ₗc[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂ :=
  DFunLike.coe_fn_eq

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