OAI/Combinatorics/Chromatic/Walls/Mass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.SlopeArithmetic.mass line 9
2. def OAI.ElementaryPositivity.SlopeArithmetic.slope line 11
3. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_add line 13
4. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_zero line 16
5. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_nonneg line 18
6. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_pos line 23
7. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_eq line 37
8. lemma OAI.ElementaryPositivity.SlopeArithmetic.add_ne_zero_left line 44
9. lemma OAI.ElementaryPositivity.SlopeArithmetic.add_ne_zero_right line 54
10. lemma OAI.ElementaryPositivity.SlopeArithmetic.slope_add line 58
11. lemma OAI.ElementaryPositivity.SlopeArithmetic.slope_add_same line 65
12. lemma OAI.ElementaryPositivity.SlopeArithmetic.slope_add_gt line 73
13. lemma OAI.ElementaryPositivity.SlopeArithmetic.mass_sum_le line 82
14. lemma OAI.ElementaryPositivity.SlopeArithmetic.destabilized_target line 97