withTopCongr_refl — Mathlib

English

For any α with a partial order, the withTop extension of the identity order is the identity extension; i.e., (OrderIso.refl α).withTopCongr = OrderIso.refl _.

Русский

Для любой частично упорядоченной множества α расширение identity с использованием withTopCongr совпадает с тождественным изоморфизмом; то есть (OrderIso.refl α).withTopCongr = OrderIso.refl _.

LaTeX

$$$(\\mathrm{OrderIso.refl}\\, \\alpha).\\mathrm{withTopCongr} = \\mathrm{OrderIso.refl}\\, \\_.$$$

Lean4

@[simp]
theorem withTopCongr_refl : (OrderIso.refl α).withTopCongr = OrderIso.refl _ :=
  RelIso.toEquiv_injective Equiv.withTopCongr_refl

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