Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.truncated_inf_of_not_mem

Modification history

2023-09-12 13:12

src/combinatorics/set_family/ahlswede_zhang.lean

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

Added finset.truncated_inf_of_not_mem View on Github →