Theorems · Definition · order theory

OrderEmbedding.ofStrictMono

{α : Type u_6} → {β : Type u_7} → [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → α ↪o β

A strictly monotone map from a linear order is an order embedding.

Defined in

Mathlib.Order.Hom.Basic

Cited by

15 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

LinearOrderPreorder