OAI/Combinatorics/Ryser/Domination/Basic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RyserCoveringCounterexample.Selection.Graph line 12
  2. theorem OAI.RyserCoveringCounterexample.Selection.Graph.irrefl line 19
  3. theorem OAI.RyserCoveringCounterexample.Selection.Graph.Adj.symm line 22
  4. def OAI.RyserCoveringCounterexample.Selection.IsTransversalOn line 30
  5. def OAI.RyserCoveringCounterexample.Selection.neighborsIn line 35
  6. theorem OAI.RyserCoveringCounterexample.Selection.mem_neighborsIn line 39
  7. theorem OAI.RyserCoveringCounterexample.Selection.neighborsIn_subset line 44
  8. theorem OAI.RyserCoveringCounterexample.Selection.neighborsIn_eq_empty_iff line 49
  9. def OAI.RyserCoveringCounterexample.Selection.DominatesOn line 60
  10. def OAI.RyserCoveringCounterexample.Selection.DominationCertificate line 64