OAI/Combinatorics/Ryser/Construction/Hypergraph.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RyserCoveringCounterexample.Construction.ConfigurationData line 12
  2. abbrev OAI.RyserCoveringCounterexample.Construction.Vertex line 20
  3. def OAI.RyserCoveringCounterexample.Construction.ordinaryVertex line 27
  4. def OAI.RyserCoveringCounterexample.Construction.specialVertex line 30
  5. def OAI.RyserCoveringCounterexample.Construction.vertexPart line 34
  6. theorem OAI.RyserCoveringCounterexample.Construction.vertexPart_ordinaryVertex line 39
  7. theorem OAI.RyserCoveringCounterexample.Construction.vertexPart_specialVertex line 42
  8. def OAI.RyserCoveringCounterexample.Construction.exceptionalVertex line 46
  9. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalVertex_of_mem line 53
  10. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalVertex_of_notMem line 59
  11. theorem OAI.RyserCoveringCounterexample.Construction.vertexPart_exceptionalVertex line 64
  12. def OAI.RyserCoveringCounterexample.Construction.ordinaryEdge line 75
  13. def OAI.RyserCoveringCounterexample.Construction.exceptionalEdge line 79
  14. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryVertex_mem_ordinaryEdge line 83
  15. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalVertex_mem_exceptionalEdge line 88
  16. theorem OAI.RyserCoveringCounterexample.Construction.selector_edge_partite line 93
  17. theorem OAI.RyserCoveringCounterexample.Construction.mem_selector_edge_iff line 104
  18. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryEdge_partite line 116
  19. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalEdge_partite line 121
  20. theorem OAI.RyserCoveringCounterexample.Construction.mem_exceptionalEdge_iff line 127
  21. def OAI.RyserCoveringCounterexample.Construction.hypergraph line 136
  22. theorem OAI.RyserCoveringCounterexample.Construction.mem_hypergraph line 142
  23. theorem OAI.RyserCoveringCounterexample.Construction.hypergraph_partite line 151
  24. theorem OAI.RyserCoveringCounterexample.Construction.hypergraph_uniform line 158
  25. theorem OAI.RyserCoveringCounterexample.Construction.hypergraph_rPartiteUniform line 162
  26. theorem OAI.RyserCoveringCounterexample.Construction.hypergraph_nonempty line 166