Commit 2024-06-25 12:23 9a2e9d33

View on Github →

refactor: Improve lemmas about sets of intermediate size (#14062) The lemmas around here are a mess. Rename Finset.exists_smaller_set to Finset.exists_subset_card_eq, Finset.exists_intermediate_set to Finset.exists_subsuperset_card_eq, and add the missing third Finset.exists_superset_card_eq. Same for Set.

Estimated changes

Modified Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.exists_subset_card_eq

added theorem Finset.exists_subsuperset_card_eq

Modified Mathlib/Data/Finset/Powerset.lean

Modified Mathlib/Data/Fintype/Card.lean

added theorem Finset.exists_superset_card_eq

Modified Mathlib/Data/Set/Card.lean

added theorem Set.exists_subset_card_eq

added theorem Set.exists_subsuperset_card_eq

modified theorem Set.ncard_coe_Finset