Theorems · Theorem · order theory

lt_csSup_of_lt

∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α}, BddAbove s → a ∈ s → b < a → b < sSup s

b < sSup s when there is an element a in s with b < a, when s is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the CompleteLattice case.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

4 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

ConditionallyCompleteLattice