Commit 2023-04-03 11:59 e90bd528

View on Github →

feat: Port/Data.List.Intervals (#1479) feat: Port/data.list.intervals

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Intervals.lean

added theorem List.Ico.append_consecutive

added theorem List.Ico.bagInter_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_le

added theorem List.Ico.filter_le_of_bot

added theorem List.Ico.filter_le_of_le

added theorem List.Ico.filter_le_of_le_bot

added theorem List.Ico.filter_le_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_succ_bot

added theorem List.Ico.filter_lt_of_top_le

added theorem List.Ico.inter_consecutive

added theorem List.Ico.length

added theorem List.Ico.map_add

added theorem List.Ico.map_sub

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.trichotomy

added theorem List.Ico.zero_bot

added def List.Ico