Theorems · Definition · order theory

StrictMono.orderIsoOfRightInverse

{α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder α] →
      [inst_1 : Preorder β] → (f : α → β) → StrictMono f → (g : β → α) → Function.RightInverse g f → α ≃o β

A strictly monotone function with a right inverse is an order isomorphism.

Defined in

Mathlib.Order.Hom.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

LinearOrderPreorder