withTopCongr_symm — Mathlib

English

For any order isomorphism e: α ≃o β, the withTopCongr of the inverse equals the inverse of the withTopCongr: e.symm.withTopCongr = e.withTopCongr.symm.

Русский

Для всякого изоморфизма порядка e: α ≃o β выполнено, что withTopCongr от обратного изоморфизма равен обратному withTopCongr: e.symm.withTopCongr = e.withTopCongr.symm.

LaTeX

$$$e^\\!-1.withTopCongr = e.withTopCongr.^{-1}$$$

Lean4

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

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