OAI/Combinatorics/Ryser/Domination/Counting.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.verticesY_subset_of_realized line 13
  2. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.pool_injOn_verticesY line 24
  3. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.image_verticesY_subset line 31
  4. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.length_le_card_verticesY line 39
  5. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.length_le_card line 50
  6. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.indices_nonempty line 54
  7. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.mem_indices_iff line 58
  8. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.vertices_pool_mem line 76
  9. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.card_verticesX_le line 89
  10. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.card_indices line 94
  11. theorem OAI.RyserCoveringCounterexample.Selection.DominationTrace.card_vertices_le line 102