OAI/Combinatorics/BalancedRyser/Probability/GeneratorEnumeration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.restrictedGeneratorLabels line 15
  2. theorem OAI.Balanced.card_restrictedGeneratorLabels line 20
  3. def OAI.Balanced.generatorLabelsWithOldCount line 31
  4. theorem OAI.Balanced.generatorLabelsWithOldCount_subset line 34
  5. theorem OAI.Balanced.card_generatorLabelsWithOldCount_le line 48
  6. def OAI.Balanced.tupleCodesWithOldCount line 65
  7. theorem OAI.Balanced.card_tupleCodesWithOldCount_le line 69
  8. theorem OAI.Balanced.exposed_generators_card_le_twenty_four line 79
  9. theorem OAI.Balanced.card_tupleCodesWithOldCount_le_uniform line 87
  10. theorem OAI.Balanced.card_tupleCodesWithOldCount_le_field line 106