InsertIdx
📁 Source: Mathlib/Data/List/InsertIdx.lean
Statistics
List
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eq_or_mem_of_mem_insertIdx 📖 | — | — | — | — | — |
eraseIdx_map 📖 | — | — | — | — | eraseIdx_pmap |
eraseIdx_pmap 📖 | — | — | — | — | — |
getElem_insertIdx_add_succ 📖 | — | — | — | — | — |
get_insertIdx_add_succ 📖 | — | — | — | — | getElem_insertIdx_add_succ |
get_insertIdx_of_lt 📖 | — | — | — | — | — |
get_insertIdx_self 📖 | — | — | — | — | — |
insertIdx_eraseIdx_getElem 📖 | — | — | — | — | insertIdx_eraseIdx_self |
insertIdx_eraseIdx_self 📖 | — | — | — | — | — |
insertIdx_injective 📖 | — | — | — | — | — |
insertIdx_pmap 📖 | mathematical | — | eq_or_mem_of_mem_insertIdx | — | eq_or_mem_of_mem_insertIdx |
insertIdx_subset_cons 📖 | — | — | — | — | eq_or_mem_of_mem_insertIdx |
map_insertIdx 📖 | — | — | — | — | eq_or_mem_of_mem_insertIdxinsertIdx_pmap |
sublist_insertIdx 📖 | — | — | — | — | — |
subset_insertIdx 📖 | — | — | — | — | sublist_insertIdx |
take_eraseIdx_eq_take_of_le 📖 | — | — | — | — | — |
take_insertIdx_eq_take_of_le 📖 | — | — | — | — | — |
---