mathlib

8818fdef - feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612)

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](https://leanprover-community.github.io/mathlib_docs/combinatorics/set_family/lym.html#finset.sum_card_slice_div_choose_le_one), by expliciting the correction term. This PR defines `finset.truncated_sup`/`finset.truncated_inf`, whose cardinalities show up in the correction term. Co-authored-by: Vladimir Ivanov <volodimir1024@gmail.com>