Intervals

📁 Source: Mathlib/Data/List/Intervals.lean

Statistics

Metric	Count
Definitions `Ico`	1
Theorems `append_consecutive`, `bagInter_consecutive`, `chain'_succ`, `eq_cons`, `eq_empty_iff`, `eq_nil_of_le`, `filter_le`, `filter_le_of_bot`, `filter_le_of_le`, `filter_le_of_le_bot`, `filter_le_of_top_le`, `filter_lt`, `filter_lt_of_ge`, `filter_lt_of_le_bot`, `filter_lt_of_succ_bot`, `filter_lt_of_top_le`, `inter_consecutive`, `isChain_succ`, `length`, `map_add`, `map_sub`, `mem`, `nodup`, `notMem_top`, `pairwise_lt`, `pred_singleton`, `self_empty`, `succ_singleton`, `succ_top`, `trichotomy`, `zero_bot`	31
Total	32

List

Definitions

Name	Category	Theorems
`Ico` 📖	CompOp	31 math math: `Ico.map_sub`, `Ico.bagInter_consecutive`, `Ico.eq_nil_of_le`, `Ico.isChain_succ`, `Ico.filter_le_of_bot`, `Ico.filter_le_of_le_bot`, `Ico.filter_lt_of_ge`, `Ico.filter_lt`, `Ico.eq_cons`, `Ico.filter_le_of_top_le`, `Ico.map_add`, `Ico.filter_lt_of_top_le`, `Ico.self_empty`, `Ico.succ_singleton`, `Ico.filter_lt_of_le_bot`, `Ico.length`, `Ico.pairwise_lt`, `Ico.filter_le_of_le`, `Ico.pred_singleton`, `Ico.append_consecutive`, `Ico.filter_lt_of_succ_bot`, `Ico.chain'_succ`, `Ico.trichotomy`, `Ico.eq_empty_iff`, `Ico.nodup`, `Ico.notMem_top`, `Ico.zero_bot`, `Ico.inter_consecutive`, `Ico.mem`, `Ico.succ_top`, `Ico.filter_le`

List.Ico

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_consecutive` 📖	mathematical	—	`List.Ico`	—	—
`bagInter_consecutive` 📖	mathematical	—	`List.Ico`	—	`List.bagInter_nil_iff_inter_nil` `inter_consecutive`
`chain'_succ` 📖	mathematical	—	`List.Ico`	—	`isChain_succ`
`eq_cons` 📖	mathematical	—	`List.Ico`	—	`append_consecutive` `succ_singleton`
`eq_empty_iff` 📖	mathematical	—	`List.Ico`	—	`length` `eq_nil_of_le`
`eq_nil_of_le` 📖	mathematical	—	`List.Ico`	—	—
`filter_le` 📖	mathematical	—	`List.Ico`	—	`le_total` `max_eq_right` `filter_le_of_le` `max_eq_left` `filter_le_of_le_bot`
`filter_le_of_bot` 📖	mathematical	—	`List.Ico`	—	`filter_lt_of_succ_bot`
`filter_le_of_le` 📖	mathematical	—	`List.Ico`	—	`le_total` `append_consecutive` `filter_le_of_top_le` `le_refl` `filter_le_of_le_bot` `eq_nil_of_le`
`filter_le_of_le_bot` 📖	mathematical	—	`List.Ico`	—	`le_trans` `mem`
`filter_le_of_top_le` 📖	mathematical	—	`List.Ico`	—	`not_le_of_gt` `lt_of_lt_of_le` `mem`
`filter_lt` 📖	mathematical	—	`List.Ico`	—	`le_total` `min_eq_left` `filter_lt_of_top_le` `min_eq_right` `filter_lt_of_ge`
`filter_lt_of_ge` 📖	mathematical	—	`List.Ico`	—	`le_total` `append_consecutive` `filter_lt_of_top_le` `le_refl` `filter_lt_of_le_bot` `eq_nil_of_le`
`filter_lt_of_le_bot` 📖	mathematical	—	`List.Ico`	—	`le_trans` `mem`
`filter_lt_of_succ_bot` 📖	mathematical	—	`List.Ico`	—	`inf_eq_right` `filter_lt` `succ_singleton`
`filter_lt_of_top_le` 📖	mathematical	—	`List.Ico`	—	`lt_of_lt_of_le` `mem`
`inter_consecutive` 📖	mathematical	—	`List.Ico`	—	`not_lt_of_ge`
`isChain_succ` 📖	mathematical	—	`List.Ico`	—	`eq_cons` `eq_nil_of_le`
`length` 📖	mathematical	—	`List.Ico`	—	—
`map_add` 📖	mathematical	—	`List.Ico`	—	`eq_1`
`map_sub` 📖	mathematical	—	`List.Ico`	—	`eq_1`
`mem` 📖	mathematical	—	`List.Ico`	—	—
`nodup` 📖	mathematical	—	`List.Ico`	—	—
`notMem_top` 📖	mathematical	—	`List.Ico`	—	—
`pairwise_lt` 📖	mathematical	—	`List.Ico`	—	—
`pred_singleton` 📖	mathematical	—	`List.Ico`	—	—
`self_empty` 📖	mathematical	—	`List.Ico`	—	`eq_nil_of_le` `le_refl`
`succ_singleton` 📖	mathematical	—	`List.Ico`	—	—
`succ_top` 📖	mathematical	—	`List.Ico`	—	`succ_singleton` `append_consecutive`
`trichotomy` 📖	mathematical	—	`List.Ico`	—	—
`zero_bot` 📖	mathematical	—	`List.Ico`	—	`eq_1`

---

← Back to Index