coe_mk — Mathlib

English

If a coalgebra morphism is built from a linear map f with compatible structure, then its underlying function is exactly f

Русский

Если коалгоморфизм строится из линейного отображения f с сопутствующей структурой, то его базовая функция равна f

LaTeX

$$$$ ((\langle f, h, h_1 \rangle : A \to_{c[R]} B) : A \to B) = f $$$$

Lean4

@[simp]
theorem coe_mk {f : A →ₗ[R] B} (h h₁) : ((⟨f, h, h₁⟩ : A →ₗc[R] B) : A → B) = f :=
  rfl

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