coe_toOrderHom — Mathlib

English

For f in CircleDeg1Lift, the function obtained by coercing f.toOrderHom to a function equals f itself; i.e., the coercion to function of f.toOrderHom coincides with f.

Русский

Для f из CircleDeg1Lift отображение, получаемое через приведение f.toOrderHom к функции, равно самому f.

LaTeX

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

Lean4

@[simp]
theorem coe_toOrderHom : ⇑f.toOrderHom = f :=
  rfl

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