OAI/Combinatorics/BalancedRyser/Construction/Hypergraph.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.PartiteHypergraph.mem_part line 10
  2. theorem OAI.Balanced.PartiteHypergraph.mem_edgeVertices line 14
  3. theorem OAI.Balanced.PartiteHypergraph.card_part line 18
  4. theorem OAI.Balanced.PartiteHypergraph.card_edgeVertices line 24
  5. theorem OAI.Balanced.PartiteHypergraph.disjoint_parts line 31
  6. theorem OAI.Balanced.PartiteHypergraph.edgeVertices_inter_part line 38
  7. theorem OAI.Balanced.PartiteHypergraph.edgeVertices_injective line 50
  8. theorem OAI.Balanced.PartiteHypergraph.edgeVertices_inter_nonempty_iff line 59
  9. theorem OAI.Balanced.PartiteHypergraph.covers_iff_inter_nonempty line 69
  10. theorem OAI.Balanced.PartiteHypergraph.part_covers line 82
  11. theorem OAI.Balanced.PartiteHypergraph.exists_cover_card line 87
  12. theorem OAI.Balanced.PartiteHypergraph.hasCoverNumber_iff line 91
  13. theorem OAI.Balanced.PartiteHypergraph.hasCoverNumber_unique line 97
  14. theorem OAI.Balanced.PartiteHypergraph.coverNumber_le_part line 105
  15. theorem OAI.Balanced.PartiteHypergraph.covers_mono line 110
  16. theorem OAI.Balanced.PartiteHypergraph.covers_empty_iff line 116
  17. theorem OAI.Balanced.PartiteHypergraph.nonisolated_iff_mem_edge line 127
  18. theorem OAI.Balanced.PartiteHypergraph.intersecting_iff line 137
  19. theorem OAI.Balanced.PartiteHypergraph.matching_card_le_one line 143
  20. theorem OAI.Balanced.PartiteHypergraph.exists_matching_card_one line 154
  21. theorem OAI.Balanced.PartiteHypergraph.intersecting_iff_distinct line 164
  22. theorem OAI.Balanced.PartiteHypergraph.exists_hasCoverNumber line 177
  23. theorem OAI.Balanced.PartiteHypergraph.hasCoverNumber_succ_iff_no_small_cover line 186