OAI/Combinatorics/BalancedRyser/Construction/CoverObstruction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CoverObstruction.card_le_sum_inter_card_of_cover line 13
  2. theorem OAI.Balanced.CoverObstruction.card_le_initial_add_sum_inter_card_of_cover line 23
  3. theorem OAI.Balanced.CoverObstruction.card_le_initial_add_capacity_of_cover line 42
  4. theorem OAI.Balanced.CoverObstruction.card_le_inter_initial_add_capacity_of_cover line 58
  5. theorem OAI.Balanced.CoverObstruction.cover_split_selected line 70
  6. theorem OAI.Balanced.CoverObstruction.card_le_pencil_capacity_of_cover line 81
  7. theorem OAI.Balanced.CoverObstruction.second_constituent_occupancy_contradiction line 91
  8. theorem OAI.Balanced.CoverObstruction.affine_line_occupancy_contradiction line 107
  9. theorem OAI.Balanced.CoverObstruction.parallel_line_occupancy_contradiction line 122
  10. theorem OAI.Balanced.CoverObstruction.cover_by_remaining_of_forced_disjoint line 137
  11. theorem OAI.Balanced.CoverObstruction.remaining_card_le_split_count_sub_one line 149
  12. theorem OAI.Balanced.CoverObstruction.remaining_card_le_three line 157
  13. theorem OAI.Balanced.CoverObstruction.eight_points_not_covered_by_three_pairs line 166
  14. theorem OAI.Balanced.CoverObstruction.eight_points_not_covered_by_two_and_four line 178
  15. theorem OAI.Balanced.CoverObstruction.parallel_pencil_cover_impossible line 187
  16. theorem OAI.Balanced.CoverObstruction.occupancy_numeric_margins line 200