OAI/Combinatorics/BalancedRyser/Probability/PatternPrefixSupport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.PatternModel.freshPrefixSupport line 12
2. lemma OAI.Balanced.PatternModel.freshPrefixSupport_nil line 15
3. lemma OAI.Balanced.PatternModel.freshPrefixSupport_cons line 18
4. lemma OAI.Balanced.PatternModel.mem_freshPrefixSupport_iff line 23
5. lemma OAI.Balanced.PatternModel.support_sdiff_subset_freshPrefixSupport line 31
6. lemma OAI.Balanced.PatternModel.disjoint_freshPrefixSupport_initial line 38
7. lemma OAI.Balanced.PatternModel.card_freshPrefixSupport_le line 45
8. lemma OAI.Balanced.PatternModel.indicator_eq_of_agree_support line 63
9. lemma OAI.Balanced.PatternModel.indicator_fixed_eq_of_agree_fresh line 71
10. lemma OAI.Balanced.PatternModel.prefix_product_fixed_eq_of_agree_fresh line 82
11. lemma OAI.Balanced.PatternModel.prefix_product_fixed_resample line 94
12. lemma OAI.Balanced.PatternModel.overlapCount_freshPrefixSupport line 104