toOrderHom_eq_coe — Mathlib

English

For any pseudo-epimorphism f, its underlying order-homomorphism component equals f; i.e., the function part of f agrees with its OrderHom representation.

Русский

Для любого псевдоэпиморфизма f соответствующая ему отображение-гомоморфизм по порядку совпадает с f; функция f совпадает с представлением как OrderHom.

LaTeX

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

Lean4

@[simp]
theorem toOrderHom_eq_coe (f : PseudoEpimorphism α β) : ⇑f.toOrderHom = f :=
  rfl

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