OAI/Combinatorics/Chromatic/Walls/HNMatrixTriangular.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.SlopeArithmetic.hnKeyLT line 11
2. def OAI.ElementaryPositivity.SlopeArithmetic.matrixPrefix line 13
3. lemma OAI.ElementaryPositivity.SlopeArithmetic.matrixPrefix_one line 16
4. lemma OAI.ElementaryPositivity.SlopeArithmetic.matrixPrefix_succ line 20
5. structure OAI.ElementaryPositivity.SlopeArithmetic.HNSplitMatrix line 25
6. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_cell_le line 31
7. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_first_row line 37
8. lemma OAI.ElementaryPositivity.SlopeArithmetic.split_tail line 67
9. theorem OAI.ElementaryPositivity.SlopeArithmetic.hn_split_triangular line 81
10. lemma OAI.ElementaryPositivity.SlopeArithmetic.list_mass_bound line 117
11. lemma OAI.ElementaryPositivity.SlopeArithmetic.list_slope_le line 124
12. lemma OAI.ElementaryPositivity.SlopeArithmetic.list_sum_ne_zero line 132
13. lemma OAI.ElementaryPositivity.SlopeArithmetic.ordered_sum_le_head line 135
14. lemma OAI.ElementaryPositivity.SlopeArithmetic.ordered_tail_lt_head line 143
15. lemma OAI.ElementaryPositivity.SlopeArithmetic.exists_uniform_cutoff line 150