OAI/Combinatorics/BalancedRyser/Probability/ParallelBlockCapacity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Configuration.parallelDesignated line 12
  2. theorem OAI.Balanced.Configuration.designated_subset_choice_line line 15
  3. theorem OAI.Balanced.Configuration.designated_card_four line 22
  4. theorem OAI.Balanced.Configuration.designated_disjoint_of_slots_ne line 28
  5. theorem OAI.Balanced.Configuration.parallelDesignated_card line 36
  6. theorem OAI.Balanced.Configuration.designated_inter_line_card_le_one line 42
  7. theorem OAI.Balanced.Configuration.designated_inter_merged_card_le_two line 51
  8. theorem OAI.Balanced.Configuration.parallelDesignated_inter_merged_card_le_two line 65
  9. theorem OAI.Balanced.Configuration.parallelDesignated_inter_regular_card_le_two line 75
  10. theorem OAI.Balanced.Configuration.parallelDesignated_block_capacity line 90
  11. theorem OAI.Balanced.Configuration.parallelDesignated_subset_points line 113