ofRelIsoLT_symm — Mathlib

English

The inverse of the order isomorphism obtained from a RelIsoLT has the same LT-relations as the inverse RelIsoLT.

Русский

Обратное отображение полученного порядкового изоморфизма имеет такие же LT-отношения, как обратное RelIsoLT.

LaTeX

$$$ (\mathrm{ofRelIsoLT}\, e)^{-1} = \mathrm{ofRelIsoLT}\, e^{-1} $$$

Lean4

@[simp]
theorem ofRelIsoLT_symm {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : (ofRelIsoLT e).symm = ofRelIsoLT e.symm :=
  rfl

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