Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 16:48 678a2b5b

View on Github →

feat(data/list,multiset,finset): monotone_filter_(left|right) (#8842)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.monotone_filter_left

added theorem finset.monotone_filter_right

Modified src/data/list/basic.lean

deleted theorem list.filter_sublist_filter

added theorem list.is_infix.filter

added theorem list.is_prefix.filter

added theorem list.is_suffix.filter

added theorem list.monotone_filter_left

added theorem list.monotone_filter_right

added theorem list.sublist.filter

Modified src/data/list/perm.lean

added theorem list.subperm.filter

Modified src/data/multiset/basic.lean

added theorem multiset.monotone_filter_left

added theorem multiset.monotone_filter_right