InsertionSort

📁 Source: PhysLean/Mathematics/List/InsertionSort.lean

Statistics

Metric	Count
Definitions `insertionSortMinPosFin`	1
Theorems `dropWhile_sorted_eq_filter`, `dropWhile_sorted_eq_filter_filter`, `filter_rel_eq_insertionSort`, `insertionSortEquiv_commute`, `insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos`, `insertionSortEquiv_insertionSort_append`, `insertionSortEquiv_orderedInsert_append`, `insertionSortMinPos_insertionSortEquiv`, `insertionSortMin_lt_length_succ`, `insertionSortMin_lt_mem_insertionSortDropMinPos`, `insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt`, `insertionSort_append_insertionSort_append`, `insertionSort_filter`, `insertionSort_insertionSort`, `insertionSort_insertionSort_append`, `insertionSort_of_eq_list`, `insertionSort_of_takeWhile_filter`, `insertionSort_orderedInsert_append`, `orderedInsert_commute`, `orderedInsert_filter_of_neg`, `orderedInsert_filter_of_pos`, `orderedInsert_length`, `takeWhile_orderedInsert`, `takeWhile_orderedInsert'`, `takeWhile_sorted_eq_filter`	25
Total	26

PhysLean.List

Definitions

Name	Category	Theorems
`insertionSortMinPosFin` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dropWhile_sorted_eq_filter` 📖	—	—	—	—	—
`dropWhile_sorted_eq_filter_filter` 📖	—	—	—	—	—
`filter_rel_eq_insertionSort` 📖	—	—	—	—	`orderedInsert_filter_of_pos` `orderedInsert_filter_of_neg`
`insertionSortEquiv_commute` 📖	mathematical	—	`insertionSortEquiv` `orderedInsert_length`	—	`orderedInsert_length` `PhysLean.Fin.equivCons_trans` `PhysLean.Fin.equivCons_succ` `orderedInsertPos_lt_length` `orderedInsertEquiv_succ` `orderedInsertEquiv_fin_succ` `takeWhile_orderedInsert` `takeWhile_orderedInsert'`
`insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos` 📖	mathematical	—	`insertionSortEquiv`	—	—
`insertionSortEquiv_insertionSort_append` 📖	mathematical	—	`insertionSortEquiv`	—	`insertionSortEquiv_congr_apply` `orderedInsert_length` `insertionSortEquiv_orderedInsert_append` `PhysLean.Fin.equivCons_succ` `insertionSort_insertionSort_append` `orderedInsertEquiv_congr`
`insertionSortEquiv_orderedInsert_append` 📖	mathematical	—	`insertionSortEquiv` `orderedInsert_length`	—	`orderedInsert_length` `insertionSortEquiv_congr` `PhysLean.Fin.equivCons_succ` `insertionSort_orderedInsert_append` `orderedInsertEquiv_congr` `insertionSortEquiv_commute`
`insertionSortMinPos_insertionSortEquiv` 📖	mathematical	—	`insertionSortEquiv` `insertionSortMinPos`	—	`insertionSortMinPos.eq_1`
`insertionSortMin_lt_length_succ` 📖	mathematical	—	`insertionSortMinPos` `insertionSortDropMinPos`	—	`insertionSortMinPos.eq_1` `eraseIdx_length'`
`insertionSortMin_lt_mem_insertionSortDropMinPos` 📖	mathematical	—	`insertionSortMin` `insertionSortDropMinPos`	—	`insertionSort_eq_insertionSortMin_cons`
`insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt` 📖	mathematical	`insertionSortDropMinPos` `insertionSortMinPosFin`	`insertionSortMin`	—	`eraseIdx_length_succ` `eraseIdx_length` `eraseIdx_get` `insertionSortEquiv_order` `insertionSortMinPos_insertionSortEquiv` `insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos`
`insertionSort_append_insertionSort_append` 📖	—	—	—	—	`insertionSort_insertionSort_append`
`insertionSort_filter` 📖	—	—	—	—	`orderedInsert_filter_of_pos` `orderedInsert_filter_of_neg`
`insertionSort_insertionSort` 📖	—	—	—	—	—
`insertionSort_insertionSort_append` 📖	—	—	—	—	`insertionSort_orderedInsert_append`
`insertionSort_of_eq_list` 📖	—	—	—	—	`takeWhile_sorted_eq_filter` `insertionSort_filter` `dropWhile_sorted_eq_filter` `dropWhile_sorted_eq_filter_filter` `filter_rel_eq_insertionSort`
`insertionSort_of_takeWhile_filter` 📖	—	—	—	—	`insertionSort_of_eq_list`
`insertionSort_orderedInsert_append` 📖	—	—	—	—	`orderedInsert_commute`
`orderedInsert_commute` 📖	—	—	—	—	—
`orderedInsert_filter_of_neg` 📖	—	—	—	—	—
`orderedInsert_filter_of_pos` 📖	—	—	—	—	—
`orderedInsert_length` 📖	—	—	—	—	—
`takeWhile_orderedInsert` 📖	—	—	—	—	—
`takeWhile_orderedInsert'` 📖	—	—	—	—	`orderedInsert_length`
`takeWhile_sorted_eq_filter` 📖	—	—	—	—	—

---

← Back to Index