OAI/Combinatorics/BalancedRyser/Construction/ConstructionPartners.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ConstructionPartners.designated_on_line line 15
  2. theorem OAI.Balanced.ConstructionPartners.partner_adjacent line 22
  3. theorem OAI.Balanced.ConstructionPartners.partner_inter_designated_card_le_one line 54
  4. theorem OAI.Balanced.ConstructionPartners.partner_inter_designated_card_le_one_of_two line 76
  5. theorem OAI.Balanced.ConstructionPartners.partner_card_le_splitMultiplicity line 83
  6. theorem OAI.Balanced.ConstructionPartners.nonsplit_line_disjoint_designatedAt line 96
  7. theorem OAI.Balanced.ConstructionPartners.constituent_not_splitLinesAt line 114
  8. theorem OAI.Balanced.ConstructionPartners.merged_inter_designatedAt_subset_partnerSet line 123
  9. theorem OAI.Balanced.ConstructionPartners.regular_block_disjoint_designatedAt line 144
  10. theorem OAI.Balanced.ConstructionPartners.merged_block_inter_designatedAt_subset_partnerSet line 154