OAI/Combinatorics/Ryser/Selection/Forbidden.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Selection.uniform_prob_projection line 14
  2. abbrev OAI.RyserCoveringCounterexample.Selection.EquationIndex line 30
  3. def OAI.RyserCoveringCounterexample.Selection.equationEvent line 33
  4. theorem OAI.RyserCoveringCounterexample.Selection.conflict_iff_equation line 38
  5. theorem OAI.RyserCoveringCounterexample.Selection.card_equationIndex_le line 47
  6. theorem OAI.RyserCoveringCounterexample.Selection.prob_conflict_le line 59
  7. theorem OAI.RyserCoveringCounterexample.Selection.prob_not_feasible_le line 85