OAI/Combinatorics/BalancedRyser/Probability/UniformOrderedSubset.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.UniformOrderedSubset.restriction_fiber_card_eq line 16
2. theorem OAI.Balanced.UniformOrderedSubset.expect_restriction line 38
3. def OAI.Balanced.UniformOrderedSubset.imageFiberEquiv line 48
4. theorem OAI.Balanced.UniformOrderedSubset.expect_embedding_by_image line 78
5. theorem OAI.Balanced.UniformOrderedSubset.expect_permutation_ordered_subset line 102
6. def OAI.Balanced.UniformOrderedSubset.enumerationEquiv line 110
7. theorem OAI.Balanced.UniformOrderedSubset.expect_equivalences_eq_permutations line 116