OAI/Combinatorics/Chromatic/Shuffle/TwoTargetFiltration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.twoTargetTransferB line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.twoTargetTransferB_filtered line 23
3. lemma OAI.ElementaryPositivity.RawShuffle.quotient_twoTargetSeries line 56
4. lemma OAI.ElementaryPositivity.RawShuffle.clearedSeparationB_cell line 69
5. lemma OAI.ElementaryPositivity.RawShuffle.clearedSeparationB_cell_constant_next line 87
6. def OAI.ElementaryPositivity.RawShuffle.clearedConstantB line 125
7. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_apply line 129
8. lemma OAI.ElementaryPositivity.RawShuffle.unitalSeparationConstant_shuffle_grid line 134
9. lemma OAI.ElementaryPositivity.RawShuffle.clearedConstantB_grid_sameSlope_support line 147