toFun_eq_coe — Mathlib

English

The underlying function of a pseudo-epimorphism f is exactly the same as the coercion to a function, i.e., f.toFun = (f : α→β).

Русский

Базовая функция псевдоэпиморфизма f совпадает с его приведением к обычной функции: f.toFun = (f : α→β).

LaTeX

$$$\forall f:\mathrm{PseudoEpimorphism}(\alpha,\beta),\ f.toFun = (f : \alpha \to \beta)$$$

Lean4

theorem toFun_eq_coe {f : PseudoEpimorphism α β} : f.toFun = (f : α → β) :=
  rfl

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