TakeDrop
📁 Source: Mathlib/Data/List/TakeDrop.lean
Statistics
List
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
cons_getElem_drop_succ 📖 | — | — | — | — | — |
cons_get_drop_succ 📖 | — | — | — | — | — |
dropSlice_eq 📖 | — | — | — | — | — |
drop_length_sub_one 📖 | — | — | — | — | — |
drop_take_append_drop 📖 | — | — | — | — | — |
drop_take_append_drop' 📖 | — | — | — | — | drop_take_append_drop |
left_eq_take_iff 📖 | — | — | — | — | take_eq_left_iff |
length_dropSlice 📖 | — | — | — | — | — |
length_dropSlice_lt 📖 | — | — | — | — | — |
span_eq_takeWhile_dropWhile 📖 | — | — | — | — | — |
takeD_eq_take 📖 | — | — | — | — | — |
takeD_left 📖 | — | — | — | — | takeD_eq_take |
takeD_left' 📖 | — | — | — | — | takeD_left |
takeD_length 📖 | — | — | — | — | — |
takeI_eq_take 📖 | mathematical | — | takeI | — | — |
takeI_left 📖 | mathematical | — | takeI | — | takeI_eq_take |
takeI_left' 📖 | mathematical | — | takeI | — | takeI_left |
takeI_length 📖 | mathematical | — | takeI | — | — |
takeI_nil 📖 | mathematical | — | takeI | — | — |
take_concat_get' 📖 | — | — | — | — | — |
take_eq_left_iff 📖 | — | — | — | — | — |
take_eq_self_iff 📖 | — | — | — | — | — |
take_one_drop_eq_of_lt_length 📖 | — | — | — | — | — |
take_self_eq_iff 📖 | — | — | — | — | take_eq_self_iff |
---