Commit 2026-08-10 13:55 425ea606

View on Github →

feat(Order/ConditionallyCompleteLattice/Finset): add sup_eq_ciSup (#41361) From the Carleson project.

Upstreaming from Carleson: /Carleson/ToMathlib/Data/Finset/Lattice/Fold.lean Changes from the Carleson version:

  1. sup_eq_iSup' is refactored (to shorten the proof & to make some of the imports unnecessary)
  2. sup_eq_iSup' is renamed to sup_eq_ciSup
  3. Carleson-suggested file was /Data/Finset/Lattice/Fold.lean, but we placed the theorem into /Order/ConditionallyCompleteLattice/Finset.lean

Estimated changes

added theorem Finset.sup_eq_ciSup
modified theorem Finset.sup_univ_eq_ciSup