Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-22 15:32 7baf093a

View on Github →

feat(data/list,data/multiset,data/finset): add Ico intervals (closes #496)

Estimated changes

Modified src/data/finset.lean

added theorem finset.Ico.card

added theorem finset.Ico.diff_left

added theorem finset.Ico.diff_right

added theorem finset.Ico.eq_cons

added theorem finset.Ico.eq_empty_iff

added theorem finset.Ico.eq_empty_of_le

added theorem finset.Ico.filter_ge

added theorem finset.Ico.filter_ge_of_ge

added theorem finset.Ico.filter_ge_of_le_bot

added theorem finset.Ico.filter_ge_of_top_le

added theorem finset.Ico.filter_lt

added theorem finset.Ico.filter_lt_of_ge

added theorem finset.Ico.filter_lt_of_le_bot

added theorem finset.Ico.filter_lt_of_top_le

added theorem finset.Ico.map_add

added theorem finset.Ico.mem

added theorem finset.Ico.not_mem_top

added theorem finset.Ico.pred_singleton

added theorem finset.Ico.self_eq_empty

added theorem finset.Ico.succ_singleton

added theorem finset.Ico.succ_top

added theorem finset.Ico.to_finset

added theorem finset.Ico.union_consecutive

added theorem finset.Ico.val

added theorem finset.Ico.zero_bot

added def finset.Ico

Modified src/data/list/basic.lean

added theorem list.Ico.append_consecutive

added theorem list.Ico.chain'_succ

added theorem list.Ico.eq_cons

added theorem list.Ico.eq_empty_iff

added theorem list.Ico.eq_nil_of_le

added theorem list.Ico.filter_ge

added theorem list.Ico.filter_ge_of_ge

added theorem list.Ico.filter_ge_of_le_bot

added theorem list.Ico.filter_ge_of_top_le

added theorem list.Ico.filter_lt

added theorem list.Ico.filter_lt_of_ge

added theorem list.Ico.filter_lt_of_le_bot

added theorem list.Ico.filter_lt_of_top_le

added theorem list.Ico.length

added theorem list.Ico.map_add

added theorem list.Ico.mem

added theorem list.Ico.nodup

added theorem list.Ico.not_mem_top

added theorem list.Ico.pairwise_lt

added theorem list.Ico.pred_singleton

added theorem list.Ico.self_empty

added theorem list.Ico.succ_singleton

added theorem list.Ico.succ_top

added theorem list.Ico.zero_bot

added def list.Ico

modified theorem list.range'_append

Modified src/data/multiset.lean

added theorem multiset.Ico.add_consecutive

added theorem multiset.Ico.card

added theorem multiset.Ico.eq_cons

added theorem multiset.Ico.eq_zero_iff

added theorem multiset.Ico.eq_zero_of_le

added theorem multiset.Ico.filter_ge

added theorem multiset.Ico.filter_ge_of_ge

added theorem multiset.Ico.filter_ge_of_le_bot

added theorem multiset.Ico.filter_ge_of_top_le

added theorem multiset.Ico.filter_lt

added theorem multiset.Ico.filter_lt_of_ge

added theorem multiset.Ico.filter_lt_of_le_bot

added theorem multiset.Ico.filter_lt_of_top_le

added theorem multiset.Ico.map_add

added theorem multiset.Ico.mem

added theorem multiset.Ico.nodup

added theorem multiset.Ico.not_mem_top

added theorem multiset.Ico.pred_singleton

added theorem multiset.Ico.self_eq_zero

added theorem multiset.Ico.succ_singleton

added theorem multiset.Ico.succ_top

added theorem multiset.Ico.zero_bot

added def multiset.Ico

added theorem multiset.coe_eq_zero