Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.filter_infs_ge

Modification history

2023-09-12 13:12
src/data/finset/sups.lean
feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612) …
Added finset.filter_infs_geView on Github →