Theorems · Theorem · order theory

DirectedOn.csInf_le_csSup

∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrder α] {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≥ x2) s →
    DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddBelow s → BddAbove s → s.Nonempty → sInf s ≤ sSup s

If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Basic

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

ConditionallyCompletePartialOrder