coe_id_orderHom — Mathlib

English

The order-hom component of the identity pseudo-epimorphism is the identity order-homomorphism.

Русский

Компонента порядка гомоморфизма тождества псевдоэпиморфизма является тождественным гомоморфизмом по порядку.

LaTeX

$$$\mathrm{coe}_{\text{id}}^{\text{orderHom}} = \mathrm{Id}$$$

Lean4

@[simp, norm_cast]
theorem coe_id_orderHom : (PseudoEpimorphism.id α : α →o α) = OrderHom.id :=
  rfl

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