OAI/Dynamics/ConditionalShuffle/Ranks.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Revealed.imageRank_lt_iff line 10
2. lemma OAI.Revealed.imageRank_comp_perm line 17
3. def OAI.Revealed.splitLabels line 36
4. lemma OAI.Revealed.splitLabels_inl line 46
5. lemma OAI.Revealed.splitLabels_inr line 47
6. def OAI.Revealed.Split.ranks line 52
7. lemma OAI.Revealed.Split.ranks_pre line 56
8. lemma OAI.Revealed.Split.ranks_assignment line 64
9. lemma OAI.Revealed.Split.ranks_freeRank line 69