Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-12 13:37 82f79a58

View on Github →

feat(data/list|multiset|finset): lemmas about intervals in nat (#795)

Estimated changes

Modified src/data/finset.lean

added theorem finset.Ico.image_add

added theorem finset.Ico.image_sub

added theorem finset.Ico.inter_consecutive

deleted theorem finset.Ico.map_add

modified theorem finset.Ico.pred_singleton

added theorem finset.Ico.succ_top'

Modified src/data/list/basic.lean

added theorem list.Ico.bag_inter_consecutive

added theorem list.Ico.inter_consecutive

added theorem list.Ico.map_sub

modified theorem list.Ico.pred_singleton

added theorem list.map_sub_range'

Modified src/data/multiset.lean

added theorem multiset.Ico.inter_consecutive

added theorem multiset.Ico.map_sub

modified theorem multiset.Ico.pred_singleton