OAI/Combinatorics/Ryser/Construction/Intersection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Construction.exists_equal_projection line 11
  2. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryEdge_inter_ordinaryEdge line 20
  3. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalEdge_inter_of_projection_eq line 28
  4. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryEdge_inter_exceptionalEdge line 38
  5. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalEdge_inter_of_separated line 49
  6. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalEdge_inter_sameGroup line 60
  7. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryEdge_injective line 99
  8. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalEdge_injective line 109
  9. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryEdge_ne_exceptionalEdge line 127
  10. theorem OAI.RyserCoveringCounterexample.Construction.exceptionalEdge_ne_of_group_ne line 138
  11. theorem OAI.RyserCoveringCounterexample.Construction.hypergraph_intersecting_of_geometric_data line 151