Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-09-12 13:12 8818fdef

View on Github →

feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612) The Ahlswede-Zhang identity is a sharpening of the Lubell-Yamamoto-Meshalkin identity, by expliciting the correction term. This PR defines finset.truncated_sup/finset.truncated_inf, whose cardinalities show up in the correction term.

Estimated changes

Created src/combinatorics/set_family/ahlswede_zhang.lean

added theorem finset.card_truncated_sup_union_add_card_truncated_sup_infs

added theorem finset.compl_truncated_inf

added theorem finset.compl_truncated_sup

added theorem finset.le_truncated_sup

added theorem finset.map_truncated_inf

added theorem finset.map_truncated_sup

added def finset.truncated_inf

added theorem finset.truncated_inf_empty

added theorem finset.truncated_inf_le

added theorem finset.truncated_inf_of_mem

added theorem finset.truncated_inf_of_not_mem

added theorem finset.truncated_inf_sups

added theorem finset.truncated_inf_sups_of_not_mem

added theorem finset.truncated_inf_union

added theorem finset.truncated_inf_union_left

added theorem finset.truncated_inf_union_of_not_mem

added theorem finset.truncated_inf_union_right

added def finset.truncated_sup

added theorem finset.truncated_sup_empty

added theorem finset.truncated_sup_infs

added theorem finset.truncated_sup_infs_of_not_mem

added theorem finset.truncated_sup_of_mem

added theorem finset.truncated_sup_of_not_mem

added theorem finset.truncated_sup_union

added theorem finset.truncated_sup_union_left

added theorem finset.truncated_sup_union_of_not_mem

added theorem finset.truncated_sup_union_right

Modified src/data/finset/sups.lean

added theorem finset.filter_infs_ge

added theorem finset.filter_sups_le

Modified src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean