coe_mks — Mathlib

English

When you nest the constructor for a coalgebra morphism, the resulting coe to A → B is the original function f

Русский

При вложении конструктора для коалгоморфизма, получаемая коэрция в A → B равна исходной функции f

LaTeX

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

Lean4

@[norm_cast]
theorem coe_mks {f : A → B} (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩ : A →ₗc[R] B) = f :=
  rfl

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