OAI/Combinatorics/BalancedRyser/Probability/EqualityPatternOrdering.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.EqualityPattern.classSet line 11
  2. theorem OAI.Balanced.Local.EqualityPattern.card_classSet line 15
  3. theorem OAI.Balanced.Local.EqualityPattern.biUnion_classSet line 20
  4. theorem OAI.Balanced.Local.EqualityPattern.card_biUnion_classSet line 30
  5. theorem OAI.Balanced.Local.EqualityPattern.sum_card_classSet line 36
  6. theorem OAI.Balanced.Local.EqualityPattern.classSet_reuse_le line 40
  7. theorem OAI.Balanced.Local.EqualityPattern.classSet_reuse_eq line 46
  8. theorem OAI.Balanced.Local.EqualityPattern.exists_smallReuseOrder line 52
  9. theorem OAI.Balanced.Local.EqualityPattern.exists_processing_perm line 60
  10. theorem OAI.Balanced.Local.EqualityPattern.generatorSet_prescribedTuple line 68
  11. theorem OAI.Balanced.Local.EqualityPattern.prescribed_generator_overlap_card line 74
  12. theorem OAI.Balanced.Local.EqualityPattern.exists_uniform_direction_order line 84
  13. theorem OAI.Balanced.Local.EqualityPattern.exists_direction_processing_perm line 94