OAI/Combinatorics/BalancedRyser/Local/FiniteLocalLemma.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.FiniteProbability.mem_avoidline 12 - theorem
OAI.Balanced.FiniteProbability.avoid_emptyline 16 - theorem
OAI.Balanced.FiniteProbability.avoid_antitoneline 20 - theorem
OAI.Balanced.FiniteProbability.avoid_insertline 28 - theorem
OAI.Balanced.FiniteProbability.mass_nonnegline 34 - theorem
OAI.Balanced.FiniteProbability.mass_monoline 38 - theorem
OAI.Balanced.FiniteProbability.mass_sdiffline 43 - theorem
OAI.Balanced.FiniteProbability.local_lemmaline 51