OAI/Combinatorics/BalancedRyser/Local/LocalFourEvents.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.FourEvents.tuplePoints line 15
  2. def OAI.Balanced.Local.FourEvents.usedDirections line 19
  3. def OAI.Balanced.Local.FourEvents.usingTuples line 22
  4. def OAI.Balanced.Local.FourEvents.classUseCount line 26
  5. theorem OAI.Balanced.Local.FourEvents.usingTuples_class_card line 30
  6. theorem OAI.Balanced.Local.FourEvents.classUseCount_pos line 36
  7. theorem OAI.Balanced.Local.FourEvents.sum_classUseCount line 42
  8. theorem OAI.Balanced.Local.FourEvents.sum_class_excess line 60
  9. theorem OAI.Balanced.Local.FourEvents.usingTuples_eq_empty_of_not_used line 71
  10. theorem OAI.Balanced.Local.FourEvents.sum_direction_excess line 81
  11. theorem OAI.Balanced.Local.FourEvents.mem_tuplePoints line 99
  12. theorem OAI.Balanced.Local.FourEvents.prescribedDesignated_eq_biUnion line 106
  13. theorem OAI.Balanced.Local.FourEvents.prescribedDesignated_card line 115
  14. theorem OAI.Balanced.Local.FourEvents.tuplePoints_subset_target line 122
  15. theorem OAI.Balanced.Local.FourEvents.tuplePoints_inter_merged_card_le_two line 130
  16. def OAI.Balanced.Local.FourEvents.Precoverage line 149
  17. def OAI.Balanced.Local.FourEvents.UsedPairExtra line 153
  18. def OAI.Balanced.Local.FourEvents.ForbiddenCollinearTriple line 158
  19. def OAI.Balanced.Local.FourEvents.UnusedNoncollinearTriple line 165
  20. theorem OAI.Balanced.Local.FourEvents.line_inter_merged_card_le_two line 171
  21. theorem OAI.Balanced.Local.FourEvents.used_pair_trace_le line 180
  22. theorem OAI.Balanced.Local.FourEvents.unused_pair_trace_le line 205
  23. def OAI.Balanced.Local.FourEvents.UnusedPrecoverage line 245
  24. theorem OAI.Balanced.Local.FourEvents.precoverage_iff_unused line 250
  25. def OAI.Balanced.Local.FourEvents.extraCapacity line 263
  26. theorem OAI.Balanced.Local.FourEvents.sum_extraCapacity line 269
  27. theorem OAI.Balanced.Local.FourEvents.allowed_piece_trace_le line 276
  28. theorem OAI.Balanced.Local.FourEvents.cover_budget_le line 311
  29. theorem OAI.Balanced.Local.FourEvents.admissibleBadCover_four_events line 345