Mathlib v3 is deprecated. Go to Mathlib v4

Theorem multiset.range_disjoint_map_add

Modification history

2021-12-13 09:36
src/data/multiset/range.lean
feat(data/{list, multiset, finset}/range): add range_add (#10706) …
Added multiset.range_disjoint_map_addView on Github →