OAI/Combinatorics/Ryser/Selection/ChunkLoss.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Selection.card_le_card_sdiff_biUnion_add_sum_card_inter line 19
  2. theorem OAI.RyserCoveringCounterexample.Selection.sum_card_le_sum_card_sdiff_biUnion_add_sum_card_inter line 28
  3. theorem OAI.RyserCoveringCounterexample.Selection.sum_card_sub_sum_card_sdiff_biUnion_le_nat line 42
  4. theorem OAI.RyserCoveringCounterexample.Selection.sum_card_sub_sum_card_sdiff_biUnion_le line 51
  5. def OAI.RyserCoveringCounterexample.Selection.chunkFeasibleSet line 68
  6. theorem OAI.RyserCoveringCounterexample.Selection.mem_chunkFeasibleSet line 74
  7. def OAI.RyserCoveringCounterexample.Selection.conflictingPoints line 81
  8. theorem OAI.RyserCoveringCounterexample.Selection.mem_conflictingPoints line 86
  9. theorem OAI.RyserCoveringCounterexample.Selection.chunkFeasibleSet_eq_sdiff_biUnion line 92
  10. theorem OAI.RyserCoveringCounterexample.Selection.chunkFeasibleSet_feasibleSet line 111
  11. theorem OAI.RyserCoveringCounterexample.Selection.sum_card_sub_sum_card_chunkFeasibleSet_le_conflictingPoints line 125
  12. theorem OAI.RyserCoveringCounterexample.Selection.card_conflictingPoints_le_equationLoss line 141
  13. theorem OAI.RyserCoveringCounterexample.Selection.sum_card_conflictingPoints_le_entryLoss line 190
  14. theorem OAI.RyserCoveringCounterexample.Selection.chunk_mass_loss_le_entryLoss line 205
  15. theorem OAI.RyserCoveringCounterexample.Selection.feasibleMass_sub_le_entryLoss line 215