Theorems · Theorem · order theory

csSup_eq_csSup_of_forall_exists_le

∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s t : Set α},
  (∀ x ∈ s, ∃ y ∈ t, x ≤ y) → (∀ y ∈ t, ∃ x ∈ s, y ≤ x) → sSup s = sSup t

When every element of a set s is bounded by an element of a set t, and conversely, then s and t have the same supremum. This holds even when the sets may be empty or unbounded.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrder