Commit 2026-09-24 15:23 0fb32918

feat: OrderSupSet (#38328) This PR introduces OrderSupSet and OrderInfSet, which are typeclasses expressing that sSup (resp., sInf) returns the least upper bound (resp., the greatest lower bound) of a set whenever one exists. This allows us to prove properties about the sSup of specific sets (such as ∅, singletons, finite sets, and univ) without any typeclasses asserting the existence of LUBs. For example, sSup ∅ = ⊥ holds for any type equipped with OrderBot OrderSupSet, no longer requiring typeclasses like ConditionallyCompleteLinearOrderBot. For a general set s, this gives a uniform way to extend results about IsLUB s a → motive a to motive (sSup s), motive (⨆ i, f i), motive (a ⊔ b), etc., which allows proof reuse for basic API such as csSup_insert, iSup_insert, and sSup_insert and downstream code like csSup_add, sSup_add, and sup_add. Furthermore, this allows us to refactor incrementally, reducing the dependency of results about various completeness typeclasses on the specific implementation of sSup.