OAI/Combinatorics/BalancedRyser/Probability/DistinctRoleLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.DistinctRole.uniform_filter_eq_map_subtype line 11
2. def OAI.Balanced.DistinctRole.distinctEquiv line 47
3. instance OAI.Balanced.DistinctRole.distinctNonempty line 69
4. theorem OAI.Balanced.DistinctRole.uniform_distinct_map_role_one line 73
5. theorem OAI.Balanced.DistinctRole.distinct_support line 84
6. theorem OAI.Balanced.DistinctRole.offsetLaw_filter_distinct_map_role_one line 90
7. theorem OAI.Balanced.DistinctRole.offsetLaw_map_role_one line 110
8. theorem OAI.Balanced.DistinctRole.map_role_one_observable line 126