OAI/Combinatorics/Ryser/Hypergraph/Matching.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.mem_matchings line 9
  2. theorem OAI.RyserCoveringCounterexample.isMatching_empty line 14
  3. theorem OAI.RyserCoveringCounterexample.isMatching_singleton line 19
  4. theorem OAI.RyserCoveringCounterexample.matchings_nonempty line 25
  5. theorem OAI.RyserCoveringCounterexample.IsMatching.card_le_matchingNumber line 28
  6. theorem OAI.RyserCoveringCounterexample.matchingNumber_le_iff line 32
  7. theorem OAI.RyserCoveringCounterexample.matchingNumber_le line 42
  8. theorem OAI.RyserCoveringCounterexample.exists_isMatching_card_eq_matchingNumber line 46
  9. theorem OAI.RyserCoveringCounterexample.matchingNumber_le_card line 52
  10. theorem OAI.RyserCoveringCounterexample.matchingNumber_empty line 57
  11. theorem OAI.RyserCoveringCounterexample.one_le_matchingNumber_of_nonempty line 61
  12. theorem OAI.RyserCoveringCounterexample.IsMatching.card_le_one_of_intersecting line 67
  13. theorem OAI.RyserCoveringCounterexample.matchingNumber_eq_one_of_nonempty_intersecting line 76