Theorems · Definition · order theory

OrderIso.toRelIsoLT

{α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2

Converts an OrderIso into a RelIso (<) (<).

Defined in

Mathlib.Order.Hom.Basic

Cited by

9 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorder