Theorems · Definition · order theory

Disjoint

{α : Type u_1} → [inst : PartialOrder α] → [OrderBot α] → α → α → Prop

Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.) Note that we define this without reference to ⊓, as this allows us to talk about orders where the infimum is not unique, or where implementing Inf would require additional Decidable arguments.

Defined in

Mathlib.Order.Disjoint

Cited by

2,201 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 11 definitions · uses no axioms

Assumes

PartialOrderOrderBot