OAI/Combinatorics/Chromatic/Shuffle/CutoffGrid.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.clipped_gridShape_nonhead_zero line 17
  2. lemma OAI.ElementaryPositivity.RawShuffle.clipped_gridShape_wrong_source line 39
  3. lemma OAI.ElementaryPositivity.RawShuffle.clipped_grid_wrong_source line 58
  4. theorem OAI.ElementaryPositivity.RawShuffle.clipped_restrict_wrong_head line 73
  5. def OAI.ElementaryPositivity.RawShuffle.headRestriction line 97
  6. lemma OAI.ElementaryPositivity.RawShuffle.headRestriction_mk line 104
  7. lemma OAI.ElementaryPositivity.RawShuffle.headRestriction_zero line 112
  8. lemma OAI.ElementaryPositivity.RawShuffle.headRestriction_ideal line 122
  9. lemma OAI.ElementaryPositivity.RawShuffle.headRestriction_shuffle_grid line 130
  10. def OAI.ElementaryPositivity.RawShuffle.fullShape line 141
  11. def OAI.ElementaryPositivity.RawShuffle.zeroShape line 142
  12. lemma OAI.ElementaryPositivity.RawShuffle.shapeComplement_full line 144
  13. lemma OAI.ElementaryPositivity.RawShuffle.zeroShape_val line 147
  14. lemma OAI.ElementaryPositivity.RawShuffle.eq_fullShape_of_complement line 149
  15. lemma OAI.ElementaryPositivity.RawShuffle.eq_zeroShape_of_val line 158
  16. lemma OAI.ElementaryPositivity.RawShuffle.clipped_grid_constant_head line 163
  17. theorem OAI.ElementaryPositivity.RawShuffle.headRestriction_shuffle_head line 192