ofRelIsoLT_toRelIsoLT — Mathlib

English

For partial orders α,β, applying toRelIsoLT to the order obtained from ofRelIsoLT returns the original RelIsoLT.

Русский

Для частичных порядков α,β применение toRelIsoLT к порядку, полученному из ofRelIsoLT, возвращает исходный RelIsoLT.

LaTeX

$$$ toRelIsoLT (ofRelIsoLT e) = e $$$

Lean4

@[simp]
theorem ofRelIsoLT_toRelIsoLT {α β} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ofRelIsoLT (toRelIsoLT e) = e :=
  by
  ext
  simp

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