withBotCongr_symm — Mathlib

English

For an order isomorphism e, taking the inverse and then applying withBotCongr equals taking withBotCongr and then taking the inverse.

Русский

Для изоморфизма e взятие обратного и применение withBotCongr даёт то же самое, что применение withBotCongr затем обратное.

LaTeX

$$$ e^{\mathrm{symm}}.{\mathrm{withBotCongr}} = e.{\mathrm{withBotCongr}}^{\mathrm{symm}} $$$

Lean4

@[simp]
theorem withBotCongr_symm (e : α ≃o β) : e.symm.withBotCongr = e.withBotCongr.symm :=
  RelIso.toEquiv_injective e.toEquiv.withBotCongr_symm

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