OAI/Combinatorics/Chromatic/Walls/HNGeometry.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.SlopeArithmetic.slopeCross line 10
2. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_zero_left line 11
3. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_zero_right line 12
4. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_add_left line 13
5. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_add_right line 15
6. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_eq line 17
7. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_pos_iff line 21
8. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_nonpos_iff line 24
9. def OAI.ElementaryPositivity.SlopeArithmetic.polygonArea line 28
10. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_nil line 31
11. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_cons line 32
12. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_singleton line 34
13. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_list_sum line 35
14. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_append line 40
15. def OAI.ElementaryPositivity.SlopeArithmetic.HNOrdered line 46
16. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_nonneg line 49
17. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_pos line 63
18. lemma OAI.ElementaryPositivity.SlopeArithmetic.polygonArea_replace line 85
19. lemma OAI.ElementaryPositivity.SlopeArithmetic.reorder_progress line 92
20. abbrev OAI.ElementaryPositivity.SlopeArithmetic.HNComposition line 118
21. def OAI.ElementaryPositivity.SlopeArithmetic.hnSize line 120
22. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnSize_add line 121
23. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnSize_zero line 122
24. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnSize_eq_zero line 123
25. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnSize_list_sum line 126
26. lemma OAI.ElementaryPositivity.SlopeArithmetic.HNComposition.length_le line 130
27. instance OAI.ElementaryPositivity.SlopeArithmetic.(instance at line 139) line 139
28. def OAI.ElementaryPositivity.SlopeArithmetic.HNBefore line 159
29. instance OAI.ElementaryPositivity.SlopeArithmetic.(instance at line 163) line 163
30. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnBefore_wellFounded line 172
31. lemma OAI.ElementaryPositivity.SlopeArithmetic.not_hnOrdered_adjacent line 175
32. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnSize_pair_lt line 194
33. lemma OAI.ElementaryPositivity.SlopeArithmetic.slopeCross_of_destabilizing line 220