Theorems · Theorem · order theory

ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed

∀ {α : Type u_3} [self : ConditionallyCompletePartialOrderSup α] (s : Set α),
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)

For each nonempty, directed set s which is bounded above, sSup s is the least upper bound of s.

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Defs

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

ConditionallyCompletePartialOrderSup