OAI/Combinatorics/Ryser/Selection/PoolCounts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Selection.targetPositions line 11
  2. theorem OAI.RyserCoveringCounterexample.Selection.mem_targetPositions line 14
  3. theorem OAI.RyserCoveringCounterexample.Selection.card_targetPositions line 19
  4. theorem OAI.RyserCoveringCounterexample.Selection.image_freshTargets_val line 24
  5. theorem OAI.RyserCoveringCounterexample.Selection.card_freshTargets_eq_sdiff line 38
  6. theorem OAI.RyserCoveringCounterexample.Selection.card_freshTargets line 45
  7. theorem OAI.RyserCoveringCounterexample.Selection.card_freshTargets_add_card line 50
  8. theorem OAI.RyserCoveringCounterexample.Selection.freshTargets_card_lower line 56
  9. theorem OAI.RyserCoveringCounterexample.Selection.sum_exposedCount line 62
  10. theorem OAI.RyserCoveringCounterexample.Selection.targetPositions_eq_filter line 70
  11. theorem OAI.RyserCoveringCounterexample.Selection.exposedCount_le line 75
  12. theorem OAI.RyserCoveringCounterexample.Selection.card_freshTargets_fiber line 92
  13. theorem OAI.RyserCoveringCounterexample.Selection.sum_freshTargets line 145