OAI/Combinatorics/BalancedRyser/Local/LocalCoverMarking.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Balanced.Local.Surplus.CoverAssignment line 17
  2. theorem OAI.Balanced.Local.Surplus.badCover_exists_assignment line 24
  3. def OAI.Balanced.Local.Surplus.pieceExtra line 50
  4. def OAI.Balanced.Local.Surplus.pieceCapacity line 55
  5. theorem OAI.Balanced.Local.Surplus.sum_pieceExtra_le line 60
  6. theorem OAI.Balanced.Local.Surplus.sum_pieceCapacity_le line 70
  7. def OAI.Balanced.Local.Surplus.assignmentFibre line 78
  8. def OAI.Balanced.Local.Surplus.protectedFibre line 83
  9. theorem OAI.Balanced.Local.Surplus.protectedFibre_subset line 91
  10. theorem OAI.Balanced.Local.Surplus.protectedFibre_card_le line 99
  11. theorem OAI.Balanced.Local.Surplus.badCover_exists_marked_surplus line 118
  12. theorem OAI.Balanced.Local.Surplus.assigned_precoverage_marked line 154
  13. theorem OAI.Balanced.Local.Surplus.assigned_merged_surplus_nonpurposeful line 164
  14. theorem OAI.Balanced.Local.Surplus.assignmentFibre_small_card_le line 178
  15. theorem OAI.Balanced.Local.Surplus.retained_eq_fibre_of_fits line 192
  16. theorem OAI.Balanced.Local.Surplus.small_piece_not_surplus line 198
  17. theorem OAI.Balanced.Local.Surplus.exists_two_anchors_of_surplus line 216
  18. theorem OAI.Balanced.Local.Surplus.assigned_surplus_two_anchors line 233