OAI/Combinatorics/BalancedRyser/Probability/DistinctPairs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.card_distinct_pairs line 17
2. theorem OAI.Balanced.card_allConstituentPairsDistinct line 29
3. theorem OAI.Balanced.finiteUniformProbability_eq_toOuterMeasure line 45
4. theorem OAI.Balanced.distinctConstituentProbability_eq line 54
5. theorem OAI.Balanced.tendsto_distinctConstituentProbability line 69