OAI/Probability/ThorpShuffle/BlockEmbedding.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Block.perm line 17

   Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:20 (same declaration text).

2. def OAI.Thorp.Block.hom line 23

   Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:26 (same declaration text).

3. def OAI.Thorp.Block.embedding line 28

   Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:31 (same declaration text).

4. def OAI.Thorp.Block.complement line 31
5. instance OAI.Thorp.Block.(instance at line 33) line 33
6. lemma OAI.Thorp.Block.card_complement line 36
7. def OAI.Thorp.Block.complementIn line 41
8. lemma OAI.Thorp.Block.complementIn_injective line 44
9. def OAI.Thorp.Block.restriction line 50
10. lemma OAI.Thorp.Block.perm_single_apply line 53
11. lemma OAI.Thorp.Block.embedding_apply line 59
12. lemma OAI.Thorp.Block.restriction_right line 62
13. lemma OAI.Thorp.Block.fixes_inside line 68
14. lemma OAI.Thorp.Block.fixes_outside_inv line 75
15. def OAI.Thorp.Block.extract line 81
16. lemma OAI.Thorp.Block.perm_extract line 95
17. lemma OAI.Thorp.Block.restriction_fiber line 106
18. lemma OAI.Thorp.Block.single_embedding_injective line 123