Commit 2026-04-05 08:48 3f56d9ab

feat(Order/ConditionallyCompleteLattice): Generalize and add cbiSup/cbiInf theorems (#37526) Generalize some theorems concerning cbiSup (⨆ i, ⨆ h : p i, f i h) by removing superfluous Nonempty typeclasses and parameters. It would be nice to also remove the BoundedAbove typeclass, but this can only be done with linear orders because junk values of lattices are not currently specified[0]. [0]: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Moving.20.60csSup.60.20junk.20into.20.60ConditionallyCompleteLattice.60/near/583143345 In the absence of that, we provide the theorem cbiSup_of_not_bddAbove defining the junk values of cbiSup in the linear order case. Add theorem cbiSup_id, showing that ⨆ i ∈ s, i = sSup s. Add theorem cbiSup_eq_of_forall_not as a counterpart to cbiSup_eq_of_forall when the condition is never true, and a corollary cbiSup_empty for the obvious empty set case. Use the new theorems to shorten the proof of cbiSup_eq_of_not_forall. Give proper names to the prime versions of ciSup_subtype and ciInf_subtype. Moves:

• ciSup_subtype' -> cbiSup_eq_ciSup_subtype
• ciInf_subtype' -> cbiInf_eq_ciInf_subtype
• ciSup_subtype'' -> ciSup_subtype_fun
• ciInf_subtype'' -> ciInf_subtype_fun