OAI/Geometry/HeilbronnTriangle/SuccessiveVectors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem355.SuccessiveVectors.exists_shortest_with_property line 10
2. theorem OAI.Problem355.SuccessiveVectors.exists_shortest_outside line 32
3. def OAI.Problem355.SuccessiveVectors.earlier line 50
4. lemma OAI.Problem355.SuccessiveVectors.earlier_snoc_castSucc line 54
5. lemma OAI.Problem355.SuccessiveVectors.earlier_snoc_last line 68
6. structure OAI.Problem355.SuccessiveVectors.IsSuccessive line 81
7. theorem OAI.Problem355.SuccessiveVectors.exists_successive line 86
8. theorem OAI.Problem355.SuccessiveVectors.exists_successive_basis line 114
9. theorem OAI.Problem355.SuccessiveVectors.IsSuccessive.monotone_norm line 123
10. theorem OAI.Problem355.SuccessiveVectors.IsSuccessive.norm_pos line 131