Theorems · Definition · order theory

Codisjoint

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

Two elements of a lattice are codisjoint if their sup is the top element. Note that we define this without reference to ⊔, as this allows us to talk about orders where the supremum is not unique, or where implementing Sup would require additional Decidable arguments.

Defined in

Mathlib.Order.Disjoint

Cited by

197 results in Mathlib

Foundations

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

Assumes

PartialOrderOrderTop