Theorems · Definition · order theory

OrderEmbedding.ofMapLEIff

{α : Type u_6} →
  {β : Type u_7} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → (f : α → β) → (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → α ↪o β

To define an order embedding from a partial order to a preorder it suffices to give a function together with a proof that it satisfies f a ≤ f b ↔ a ≤ b.

Defined in

Mathlib.Order.Hom.Basic

Cited by

6 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

PartialOrderPreorder