toRelIsoLT_ofRelIsoLT — Mathlib

English

The same relation as above, expressing that converting back and forth recovers the original RelIsoLT.

Русский

То же самое отношение, показывающее, что возврат к RelIsoLT восстанавливает исходное отношение.

LaTeX

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

Lean4

@[simp]
theorem toRelIsoLT_ofRelIsoLT {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) : toRelIsoLT (ofRelIsoLT e) = e :=
  by
  ext
  simp

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