Theorems · Definition · order theory

StrictMono.orderIsoOfSurjective

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

A strictly monotone surjective function from a linear order is an order isomorphism.

Defined in

Mathlib.Order.Hom.Set

Cited by

8 results in Mathlib

Foundations

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

Assumes

LinearOrderPreorder