Theorems · Theorem · order theory

OrderIso.toRelIsoLT_ofRelIsoLT

∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  (e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2), (OrderIso.ofRelIsoLT e).toRelIsoLT = e

Defined in

Mathlib.Order.Hom.Basic

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderPartialOrder