Commit 2025-12-13 11:44 38fef684

View on Github →

chore(Data/Finset): Rename filter_neg to filter_not (#32582) Make namings of several theorems consistent. Filter.neg has a different meaning https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Pointwise.html#Filter.instNeg

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

Modified Mathlib/Algebra/GCDMonoid/Finset.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/Combinatorics/Additive/VerySmallDoubling.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/Down.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Modified Mathlib/Combinatorics/SetFamily/KruskalKatona.lean

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

Modified Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean

Modified Mathlib/Data/Finset/Basic.lean

deleted theorem Finset.disjoint_filter_filter_neg

added theorem Finset.disjoint_filter_filter_not

deleted theorem Finset.filter_union_filter_neg_eq

added theorem Finset.filter_union_filter_not_eq

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_filter_add_card_filter_not

deleted theorem Finset.filter_card_add_filter_neg_card_eq_card

Modified Mathlib/Data/Finset/Density.lean

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/Order/Partition/Equipartition.lean