Theorems · Theorem · order theory

csSup_eq_of_forall_le_of_forall_lt_exists_gt

∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
  s.Nonempty → (∀ a ∈ s, a ≤ b) → (∀ w < b, ∃ a ∈ s, w < a) → sSup s = b

Introduction rule to prove that b is the supremum of s: it suffices to check that b is larger than all elements of s, and that this is not the case of any w<b. See sSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

8 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ConditionallyCompleteLattice