OAI/Probability/SignedSweeps/YoungCorners.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.IsRowCorner line 9
2. lemma OAI.SignedSweeps.rowCorner_mem line 12
3. lemma OAI.SignedSweeps.rowCorner_max line 18
4. def OAI.SignedSweeps.eraseRowCorner line 35
5. lemma OAI.SignedSweeps.eraseRowCorner_le line 47
6. lemma OAI.SignedSweeps.eraseRowCorner_card line 52
7. lemma OAI.SignedSweeps.eraseRowCorner_rowLen line 57
8. def OAI.SignedSweeps.predecessorPartition line 73
9. lemma OAI.SignedSweeps.predecessorPartition_injective line 77