OAI/Combinatorics/Ryser/Selection/PoolGraph.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Selection.candidateGraph line 10
  2. theorem OAI.RyserCoveringCounterexample.Selection.candidateGraph_adj line 16
  3. theorem OAI.RyserCoveringCounterexample.Selection.compatibleChoice_of_transversal line 21
  4. theorem OAI.RyserCoveringCounterexample.Selection.transversal_of_compatibleChoice line 41
  5. theorem OAI.RyserCoveringCounterexample.Selection.transversal_iff_hasCompatibleChoice line 63
  6. theorem OAI.RyserCoveringCounterexample.Selection.position_fst_surjective line 72
  7. theorem OAI.RyserCoveringCounterexample.Selection.not_hasCompatibleChoice_domination line 76
  8. theorem OAI.RyserCoveringCounterexample.Selection.not_feasible_of_dominates line 87
  9. theorem OAI.RyserCoveringCounterexample.Selection.not_hasCompatibleChoice_obstruction line 96