OAI/Combinatorics/Ryser/Hypergraph/Cover.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.IsCover.mono line 12
  2. theorem OAI.RyserCoveringCounterexample.IsCover.nonemptyEdges line 18
  3. theorem OAI.RyserCoveringCounterexample.NonemptyEdges.isCover_biUnion line 24
  4. theorem OAI.RyserCoveringCounterexample.NonemptyEdges.exists_cover line 30
  5. theorem OAI.RyserCoveringCounterexample.exists_cover_iff_nonemptyEdges line 34
  6. theorem OAI.RyserCoveringCounterexample.nonemptyEdges_iff_empty_not_mem line 38
  7. theorem OAI.RyserCoveringCounterexample.IsCover.coverNumber_le line 49
  8. theorem OAI.RyserCoveringCounterexample.exists_minimum_cover_of_exists line 53
  9. theorem OAI.RyserCoveringCounterexample.exists_minimum_cover line 59
  10. theorem OAI.RyserCoveringCounterexample.le_coverNumber_of_exists line 63
  11. theorem OAI.RyserCoveringCounterexample.le_coverNumber line 69
  12. theorem OAI.RyserCoveringCounterexample.coverNumber_le_iff line 73
  13. theorem OAI.RyserCoveringCounterexample.coverNumber_eq_zero_of_empty_mem line 82
  14. theorem OAI.RyserCoveringCounterexample.coverNumber_empty line 90
  15. theorem OAI.RyserCoveringCounterexample.coverNumber_pos line 94
  16. theorem OAI.RyserCoveringCounterexample.Intersecting.isCover_edge line 103
  17. theorem OAI.RyserCoveringCounterexample.coverNumber_le_edge_card line 113
  18. theorem OAI.RyserCoveringCounterexample.coverNumber_eq_rank_of_no_small_cover line 117