toOrderIso_toEquiv — Mathlib

English

The order isomorphism produced from an equivalence corresponds to the original equivalence.

Русский

Порядковый изоморфизм, полученный из эквивалентности, соответствует исходной эквивалентости.

LaTeX

$$$ (e^{\mathrm{toOrderIso}})^{\mathrm{toEquiv}} = e $$$

Lean4

@[simp]
theorem toOrderIso_toEquiv (e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) : (e.toOrderIso h₁ h₂).toEquiv = e :=
  rfl

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