withBotCongr_refl — Mathlib

English

The withBotCongr construction sends a identity isomorphism to the identity isomorphism on WithBot.

Русский

Конструкция withBotCongr отправляет тождественный изоморфизм в тождественный изоморфизм на WithBot.

LaTeX

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

Lean4

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

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