InsertIdx
📁 Source: PhysLean/Mathematics/List/InsertIdx.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 14 | |
| Total | 14 |
PhysLean.List
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
drop_eraseIdx_succ 📖 | — | — | — | — | — |
eraseIdx_sorted 📖 | — | — | — | — | — |
get_eq_insertIdx_succAbove 📖 | mathematical | — | insertIdx_length_fin | — | insertIdx_length_fininsertIdx_getElem_fin |
insertIdx_eq_take_drop 📖 | — | — | — | — | — |
insertIdx_eraseIdx_fin 📖 | — | — | — | — | — |
insertIdx_getElem_fin 📖 | mathematical | — | insertIdx_length_fin | — | insertIdx_length_fin |
insertIdx_length_fin 📖 | — | — | — | — | — |
insertIdx_length_fst_append 📖 | — | — | — | — | — |
insertIdx_map 📖 | — | — | — | — | — |
mem_eraseIdx_nodup 📖 | — | — | — | — | — |
take_eraseIdx_same 📖 | — | — | — | — | — |
take_insert_gt 📖 | — | — | — | — | — |
take_insert_let 📖 | — | — | — | — | — |
take_insert_same 📖 | — | — | — | — | — |
---