Commit 2023-09-05 14:01 99d76919

feat: change junk value for supremum of unbounded sets (#6870) We switch from sSup univ to sSup ∅ for the supremum of unbounded sets in a conditionally complete linear order. These quantities already coincide for all concrete instances in mathlib. With the new convention one gets additionally the theorem

theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅

which will be convenient for general measurability statements.