OAI/Combinatorics/Chromatic/Shuffle/OriginalDegree.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.properSourceFiltration_component_mem line 13
  2. def OAI.ElementaryPositivity.RawShuffle.associatedComponent line 24
  3. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_mk line 30
  4. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_twice line 37
  5. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_finite line 54
  6. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_negative line 61
  7. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_upper line 69
  8. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_finite_decomposition line 83
  9. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_primitive line 108
  10. def OAI.ElementaryPositivity.RawShuffle.originalFilteredPiece line 129
  11. lemma OAI.ElementaryPositivity.RawShuffle.originalFilteredPiece_antitone line 133
  12. lemma OAI.ElementaryPositivity.RawShuffle.originalFilteredPiece_lower line 138
  13. lemma OAI.ElementaryPositivity.RawShuffle.originalFilteredPiece_upper line 143
  14. lemma OAI.ElementaryPositivity.RawShuffle.associatedComponent_rank_eq line 154
  15. theorem OAI.ElementaryPositivity.RawShuffle.sourceHilbert_filtration line 165