coe_toOrderHom — Mathlib

English

For any continuous order homomorphism f, the underlying function of its associated order-homomorphism equals f.

Русский

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

LaTeX

$$$\uparrow f.toOrderHom = f$$$

Lean4

@[simp]
theorem coe_toOrderHom (f : α →Co β) : ⇑f.toOrderHom = f :=
  rfl

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