List

📁 Source: PhysLean/Mathematics/List.lean

Statistics

Metric	Count
Definitions `insertionSortDropMinPos`, `insertionSortEquiv`, `insertionSortMin`, `insertionSortMinPos`, `optionErase`, `optionEraseZ`, `orderedInsertEquiv`, `orderedInsertPos`	8
Theorems `dropWile_eraseIdx`, `eraseIdx_cons_length`, `eraseIdx_get`, `eraseIdx_insertionSort`, `eraseIdx_insertionSort_fin`, `eraseIdx_length`, `eraseIdx_length'`, `eraseIdx_length_succ`, `get_eq_orderedInsertEquiv`, `gt_orderedInsertPos_rel`, `insertionSortEquiv_congr`, `insertionSortEquiv_congr_apply`, `insertionSortEquiv_get`, `insertionSortEquiv_order`, `insertionSortMin_eq_insertionSort_head`, `insertionSort_eq_insertionSortMin_cons`, `insertionSort_eq_ofFn`, `insertionSort_get_comp_insertionSortEquiv`, `insertionSort_length`, `lt_orderedInsertPos_rel`, `lt_orderedInsertPos_rel_fin`, `mem_take_finrange`, `optionEraseZ_ext`, `optionEraseZ_some_length`, `orderedInsertEquiv_congr`, `orderedInsertEquiv_fin_succ`, `orderedInsertEquiv_get`, `orderedInsertEquiv_monotone_fin_succ`, `orderedInsertEquiv_sigma`, `orderedInsertEquiv_succ`, `orderedInsertEquiv_zero`, `orderedInsertPos_cons`, `orderedInsertPos_drop`, `orderedInsertPos_drop_eq_orderedInsert`, `orderedInsertPos_lt_length`, `orderedInsertPos_sigma`, `orderedInsertPos_succ_take_orderedInsert`, `orderedInsertPos_take`, `orderedInsertPos_take_eq_orderedInsert`, `orderedInsertPos_take_orderedInsert`, `orderedInsert_eq_insertIdx_orderedInsertPos`, `orderedInsert_eraseIdx_lt_orderedInsertPos`, `orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ`, `orderedInsert_eraseIdx_orderedInsertEquiv_succ`, `orderedInsert_eraseIdx_orderedInsertEquiv_zero`, `orderedInsert_eraseIdx_orderedInsertPos`, `orderedInsert_eraseIdx_orderedInsertPos_le`, `orderedInsert_get_lt`, `orderedInsert_get_orderedInsertPos`, `takeWile_eraseIdx`	50
Total	58

PhysLean.List

Definitions

Name	Category	Theorems
`insertionSortDropMinPos` 📖	CompOp	3 math math: `insertionSort_eq_insertionSortMin_cons`, `insertionSortMin_lt_mem_insertionSortDropMinPos`, `insertionSortMin_lt_length_succ`
`insertionSortEquiv` 📖	CompOp	14 math math: `eraseIdx_insertionSort_fin`, `insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos`, `insertionSortEquiv_congr`, `insertionSort_get_comp_insertionSortEquiv`, `insertionSortMinPos_insertionSortEquiv`, `insertionSort_eq_ofFn`, `insertionSortEquiv_commute`, `insertionSortEquiv_congr_apply`, `Wick.koszulSign_eraseIdx`, `insertionSortEquiv_insertionSort_append`, `insertionSortEquiv_orderedInsert_append`, `eraseIdx_insertionSort`, `insertionSortEquiv_get`, `Wick.koszulSign_insertIdx`
`insertionSortMin` 📖	CompOp	5 math math: `Wick.koszulSign_eraseIdx_insertionSortMinPos`, `insertionSortMin_eq_insertionSort_head`, `insertionSort_eq_insertionSortMin_cons`, `insertionSortMin_lt_mem_insertionSortDropMinPos`, `insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt`
`insertionSortMinPos` 📖	CompOp	3 math math: `Wick.koszulSign_eraseIdx_insertionSortMinPos`, `insertionSortMinPos_insertionSortEquiv`, `insertionSortMin_lt_length_succ`
`optionErase` 📖	CompOp	—
`optionEraseZ` 📖	CompOp	6 math math: `WickContraction.wickTerm_insert_some`, `WickContraction.staticWickTerm_insert_zero_some`, `optionEraseZ_ext`, `FieldSpecification.WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum`, `optionEraseZ_some_length`, `FieldSpecification.WickAlgebra.normalOrder_uncontracted_some`
`orderedInsertEquiv` 📖	CompOp	10 math math: `orderedInsert_eraseIdx_orderedInsertEquiv_succ`, `orderedInsertEquiv_fin_succ`, `orderedInsertEquiv_succ`, `orderedInsertEquiv_congr`, `get_eq_orderedInsertEquiv`, `orderedInsert_eraseIdx_orderedInsertEquiv_zero`, `orderedInsertEquiv_get`, `orderedInsertEquiv_zero`, `orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ`, `orderedInsertEquiv_sigma`
`orderedInsertPos` 📖	CompOp	16 math math: `orderedInsertPos_take_eq_orderedInsert`, `orderedInsertPos_drop_eq_orderedInsert`, `Wick.koszulSignInsert_eq_exchangeSign_take`, `orderedInsertPos_take_orderedInsert`, `orderedInsertPos_lt_length`, `orderedInsertPos_sigma`, `orderedInsertPos_succ_take_orderedInsert`, `orderedInsertPos_take`, `orderedInsertEquiv_fin_succ`, `orderedInsertEquiv_succ`, `orderedInsert_get_orderedInsertPos`, `orderedInsertPos_cons`, `orderedInsertEquiv_zero`, `orderedInsert_eq_insertIdx_orderedInsertPos`, `orderedInsert_eraseIdx_orderedInsertPos`, `orderedInsertPos_drop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dropWile_eraseIdx` 📖	—	—	—	—	—
`eraseIdx_cons_length` 📖	—	—	—	—	—
`eraseIdx_get` 📖	mathematical	—	`eraseIdx_length`	—	`eraseIdx_length`
`eraseIdx_insertionSort` 📖	mathematical	—	`insertionSortEquiv`	—	`PhysLean.Fin.equivCons_zero` `orderedInsertEquiv_zero` `orderedInsert_eraseIdx_orderedInsertPos` `PhysLean.Fin.equivCons_succ` `orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ`
`eraseIdx_insertionSort_fin` 📖	mathematical	—	`insertionSortEquiv`	—	`eraseIdx_insertionSort`
`eraseIdx_length` 📖	—	—	—	—	—
`eraseIdx_length'` 📖	—	—	—	—	—
`eraseIdx_length_succ` 📖	—	—	—	—	—
`get_eq_orderedInsertEquiv` 📖	mathematical	—	`orderedInsertEquiv`	—	`orderedInsertEquiv_zero` `orderedInsert_get_orderedInsertPos` `orderedInsertPos_lt_length` `orderedInsertEquiv_succ` `orderedInsert_get_lt`
`gt_orderedInsertPos_rel` 📖	—	`orderedInsertPos`	—	—	`orderedInsertPos_succ_take_orderedInsert` `orderedInsertPos_drop_eq_orderedInsert`
`insertionSortEquiv_congr` 📖	mathematical	—	`insertionSortEquiv`	—	—
`insertionSortEquiv_congr_apply` 📖	mathematical	—	`insertionSortEquiv`	—	`insertionSortEquiv_congr`
`insertionSortEquiv_get` 📖	mathematical	—	`insertionSortEquiv`	—	`insertionSortEquiv.eq_2` `orderedInsertEquiv_get`
`insertionSortEquiv_order` 📖	—	`insertionSortEquiv`	—	—	`orderedInsertEquiv_zero` `insertionSortEquiv_get` `lt_orderedInsertPos_rel_fin` `PhysLean.Fin.equivCons_zero` `insertionSortEquiv.eq_2` `orderedInsertEquiv_monotone_fin_succ` `PhysLean.Fin.equivCons_succ`
`insertionSortMin_eq_insertionSort_head` 📖	mathematical	—	`insertionSortMin` `insertionSort_length`	—	`insertionSort_length` `insertionSortEquiv_get`
`insertionSort_eq_insertionSortMin_cons` 📖	mathematical	—	`insertionSortMin` `insertionSortDropMinPos`	—	`insertionSortDropMinPos.eq_1` `eraseIdx_insertionSort_fin` `insertionSortMinPos.eq_1` `insertionSort_length` `insertionSortMin_eq_insertionSort_head`
`insertionSort_eq_ofFn` 📖	mathematical	—	`insertionSortEquiv`	—	`insertionSortEquiv_get`
`insertionSort_get_comp_insertionSortEquiv` 📖	mathematical	—	`insertionSortEquiv`	—	`insertionSortEquiv_get`
`insertionSort_length` 📖	—	—	—	—	—
`lt_orderedInsertPos_rel` 📖	—	`orderedInsertPos`	—	—	`orderedInsertPos_take`
`lt_orderedInsertPos_rel_fin` 📖	—	`orderedInsertPos`	—	—	`orderedInsertPos_take_eq_orderedInsert` `orderedInsertPos_take`
`mem_take_finrange` 📖	—	—	—	—	—
`optionEraseZ_ext` 📖	mathematical	—	`optionEraseZ`	—	—
`optionEraseZ_some_length` 📖	mathematical	—	`optionEraseZ`	—	—
`orderedInsertEquiv_congr` 📖	mathematical	—	`orderedInsertEquiv`	—	—
`orderedInsertEquiv_fin_succ` 📖	mathematical	—	`orderedInsertEquiv` `orderedInsertPos` `orderedInsertPos_lt_length`	—	`orderedInsertPos_lt_length` `PhysLean.Fin.finExtractOne_apply_neq` `PhysLean.Fin.finExtractOne_symm_inr_apply`
`orderedInsertEquiv_get` 📖	mathematical	—	`orderedInsertEquiv`	—	`get_eq_orderedInsertEquiv`
`orderedInsertEquiv_monotone_fin_succ` 📖	—	`orderedInsertEquiv`	—	—	`orderedInsertPos_lt_length` `orderedInsertEquiv_fin_succ`
`orderedInsertEquiv_sigma` 📖	mathematical	—	`orderedInsertEquiv`	—	`orderedInsertEquiv_zero` `orderedInsertPos_sigma` `orderedInsertPos_lt_length` `orderedInsertEquiv_succ`
`orderedInsertEquiv_succ` 📖	mathematical	—	`orderedInsertEquiv` `orderedInsertPos` `orderedInsertPos_lt_length`	—	`orderedInsertPos_lt_length` `PhysLean.Fin.finExtractOne_apply_neq` `PhysLean.Fin.finExtractOne_symm_inr_apply`
`orderedInsertEquiv_zero` 📖	mathematical	—	`orderedInsertEquiv` `orderedInsertPos`	—	`orderedInsertPos_lt_length` `PhysLean.Fin.finExtractOne_apply_eq` `PhysLean.Fin.finExtractOne_symm_inl_apply`
`orderedInsertPos_cons` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsertPos_drop` 📖	mathematical	—	`orderedInsertPos`	—	`orderedInsertPos_drop_eq_orderedInsert`
`orderedInsertPos_drop_eq_orderedInsert` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsertPos_lt_length` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsertPos_sigma` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsertPos_succ_take_orderedInsert` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsertPos_take` 📖	mathematical	—	`orderedInsertPos`	—	`orderedInsertPos_take_eq_orderedInsert` `orderedInsertPos_take_orderedInsert`
`orderedInsertPos_take_eq_orderedInsert` 📖	mathematical	—	`orderedInsertPos`	—	`orderedInsertPos_lt_length` `orderedInsert_get_lt`
`orderedInsertPos_take_orderedInsert` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsert_eq_insertIdx_orderedInsertPos` 📖	mathematical	—	`orderedInsertPos`	—	`orderedInsertPos_lt_length` `orderedInsertEquiv_get` `PhysLean.Fin.finExtractOne_apply_eq` `PhysLean.Fin.finExtractOne_symm_inl_apply` `orderedInsertEquiv_succ`
`orderedInsert_eraseIdx_lt_orderedInsertPos` 📖	—	`orderedInsertPos`	—	—	`takeWile_eraseIdx` `dropWile_eraseIdx`
`orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ` 📖	mathematical	—	`orderedInsertEquiv`	—	`orderedInsert_eraseIdx_orderedInsertEquiv_succ`
`orderedInsert_eraseIdx_orderedInsertEquiv_succ` 📖	mathematical	—	`orderedInsertEquiv`	—	`orderedInsertPos_lt_length` `orderedInsertEquiv_succ` `orderedInsert_eraseIdx_lt_orderedInsertPos` `orderedInsert_eraseIdx_orderedInsertPos_le`
`orderedInsert_eraseIdx_orderedInsertEquiv_zero` 📖	mathematical	—	`orderedInsertEquiv`	—	`orderedInsertPos_lt_length` `PhysLean.Fin.finExtractOne_apply_eq` `PhysLean.Fin.finExtractOne_symm_inl_apply` `orderedInsert_eraseIdx_orderedInsertPos`
`orderedInsert_eraseIdx_orderedInsertPos` 📖	mathematical	—	`orderedInsertPos`	—	—
`orderedInsert_eraseIdx_orderedInsertPos_le` 📖	—	`orderedInsertPos`	—	—	`takeWile_eraseIdx` `dropWile_eraseIdx` `orderedInsertPos.eq_1`
`orderedInsert_get_lt` 📖	—	`orderedInsertPos`	—	—	—
`orderedInsert_get_orderedInsertPos` 📖	mathematical	—	`orderedInsertPos`	—	—
`takeWile_eraseIdx` 📖	—	—	—	—	—

---

← Back to Index