toFun_eq_coe — Mathlib

English

For any morphism f, the internal function component equals the externally viewed function, i.e., the toFun part is the same as the natural function view.

Русский

Для любого отображения f компоненту toFun совпадает с обычной функцией, на которую оно смотрится как на отображение.

LaTeX

$$$f.toFun = \hat f$$$

Lean4

@[simp]
theorem toFun_eq_coe (f : A →ₛₙₐ[φ] B) : f.toFun = ⇑f :=
  rfl

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