Theorems · Theorem · order theory

Disjoint.of_orderEmbedding

∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ↪o β) [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] {a₁ a₂ : α}, Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂

If the images by an order embedding of two elements are disjoint, then they are themselves disjoint.

Defined in

Mathlib.Order.Hom.Basic

Cited by

3 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

PartialOrderPartialOrderOrderBotOrderBot