OAI/Combinatorics/BalancedRyser/Probability/ConditionalRestriction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Balanced.ConditionalRestriction.FixedArray line 14
2. instance OAI.Balanced.ConditionalRestriction.(instance at line 17) line 17
3. def OAI.Balanced.ConditionalRestriction.fixedFreshEquiv line 20
4. def OAI.Balanced.ConditionalRestriction.fixedRestrict line 37
5. def OAI.Balanced.ConditionalRestriction.freshEmbedding line 41
6. theorem OAI.Balanced.ConditionalRestriction.fixedRestriction_commutes line 49
7. theorem OAI.Balanced.ConditionalRestriction.uniform_fixed_restrict line 61
8. theorem OAI.Balanced.ConditionalRestriction.fixed_supported line 70
9. theorem OAI.Balanced.ConditionalRestriction.uniform_fixed_filter line 75
10. theorem OAI.Balanced.ConditionalRestriction.uniform_conditional_restrict line 83