Commit 2026-05-15 11:00 c8f0c84e

View on Github →

feat(Order/ConditionallyCompleteLattice/Indexed): iSup of sups vs sup of iSups (#36169) ciSup_sup_eq/ciInf_inf_eq match CompleteLattice's iSup_sup_eq/iInf_inf_eq, and in a ConditionallyCompleteLinearOrder we get an inequality without any bounded assumptions. Finset.ciSup_union for ConditionallyCompleteLinearOrderBot matches CompleteLattice's Finset.iSup_union.

Estimated changes

added theorem bbdAbove_range_sup
added theorem bbdAbove_range_sup_iff
added theorem Finset.ciSup_union
added theorem ciInf_inf_eq
added theorem ciInf_inf_le
added theorem ciSup_sup_eq
added theorem ciSup_sup_le