Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 13:40 b8faf130

View on Github →

feat(data/finset/basic): add finset.filter_eq_self (#12717) and an epsilon of cleanup from flt-regular

Estimated changes

modified theorem finset.filter_eq_empty_iff
added theorem finset.filter_eq_self
modified theorem finset.monotone_filter_left