coe_coe — Mathlib

English

The two ways of viewing a morphism as a function coincide: the coercion to a function agrees with the FunLike coe.

Русский

Два способа рассмотреть отображение как функцию совпадают: приведение к функции совпадает с коэры FunLike.

LaTeX

$$$f.toFun = \mathrm{coe}(f)$$$

Lean4

@[simp]
protected theorem coe_coe {F : Type*} [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] (f : F) :
    ⇑(f : A →ₛₙₐ[φ] B) = f :=
  rfl

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