OAI/Combinatorics/Chromatic/Walls/HNRestrictionOrder.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_sum line 11
2. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_mono line 15
3. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_eq_of_le line 19
4. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_row_slope_le line 27
5. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_row_max_zero line 39
6. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_row_max_single line 55
7. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_row_equal_key line 71
8. def OAI.ElementaryPositivity.SlopeArithmetic.clippedSlope line 87
9. lemma OAI.ElementaryPositivity.SlopeArithmetic.clippedSlope_of_le line 88
10. lemma OAI.ElementaryPositivity.SlopeArithmetic.clippedSlope_of_ge line 90
11. lemma OAI.ElementaryPositivity.SlopeArithmetic.clippedSlope_le line 92
12. lemma OAI.ElementaryPositivity.SlopeArithmetic.clipped_mass_bound line 93
13. lemma OAI.ElementaryPositivity.SlopeArithmetic.clipped_high_mass line 98
14. lemma OAI.ElementaryPositivity.SlopeArithmetic.clipped_split_destabilizes line 108
15. lemma OAI.ElementaryPositivity.RawShuffle.clipped_destabilizingSpace_eq line 131
16. lemma OAI.ElementaryPositivity.RawShuffle.clipped_gridShape_zero line 146
17. lemma OAI.ElementaryPositivity.RawShuffle.clipped_grid_zero line 164
18. theorem OAI.ElementaryPositivity.RawShuffle.clipped_restrict_high line 178
19. lemma OAI.ElementaryPositivity.RawShuffle.clipped_restrict_ideal line 191