Theorems · Theorem · order theory

csInf_le_csSup

∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  s.Nonempty →
    autoParam (BddBelow s) csInf_le_csSup._auto_1 → autoParam (BddAbove s) csInf_le_csSup._auto_3 → 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.ConditionallyCompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLattice