OAI/Combinatorics/BalancedRyser/Probability/ProductSubsetVariance.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.WithoutReplacement.finiteVariance_productline 9 - theorem
OAI.Balanced.WithoutReplacement.abs_expect_sub_expect_leline 25 - theorem
OAI.Balanced.WithoutReplacement.finiteVariance_powersetCard_product_leline 31