# 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.