Commit 2026-05-29 12:25 22bbd29b

View on Github →

chore(Data/Finset/Lattice/Fold): rename comp_sup_* to apply_sup_* (#37185) These lemmas are of the form g (s.sup f) = s.sup (g ∘ f) with no composition on the LHS.

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Finset.lean

Modified Mathlib/Analysis/CStarAlgebra/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Ultra.lean

Modified Mathlib/Data/ENNReal/Lemmas.lean

Modified Mathlib/Data/Finset/Lattice/Fold.lean

added theorem Finset.apply_sup'_eq_sup'_comp

added theorem Finset.apply_sup_eq_sup_comp

added theorem Finset.apply_sup_eq_sup_comp_of_linearOrder

deleted theorem Finset.comp_sup'_eq_sup'_comp

deleted theorem Finset.comp_sup_eq_sup_comp

deleted theorem Finset.comp_sup_eq_sup_comp_of_is_total

Modified Mathlib/Data/Finset/Max.lean

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/Order/PartialSups.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

Modified Mathlib/Topology/ContinuousMap/Ordered.lean