toFun_as_coe — Mathlib

English

For any e: α ≃ β, the forward map toFun(e) equals the underlying function e, i.e., the forward component coincides with the function underlying the equivalence.

Русский

Для любой e: α ≃ β отображение forward равно функции, лежащей в основании эквивалентности; то есть toFun(e) совпадает с функцией e.

LaTeX

$$$\forall e:\alpha \simeq \beta,\ toFun(e) = e$$$

Lean4

@[simp, mfld_simps]
theorem toFun_as_coe (e : α ≃ β) : e.toFun = e :=
  rfl

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