OAI/Combinatorics/Ryser/Construction/CoordinateCompatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Construction.projection_cubeMap_axis_eq_iff line 14
2. theorem OAI.RyserCoveringCounterexample.Construction.projection_placedPoint_cubeMap_axis_eq_iff line 24
3. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_incidence_axis_of_placed_incidence line 34
4. theorem OAI.RyserCoveringCounterexample.Construction.placedPoint_eq_of_incidence_of_direction_outside line 47
5. theorem OAI.RyserCoveringCounterexample.Construction.placedPoint_eq_of_incidence_outside_altered_axis line 62
6. def OAI.RyserCoveringCounterexample.Construction.placedConfiguration line 74
7. theorem OAI.RyserCoveringCounterexample.Construction.placedExceptionalEdge_inter_sameGroup line 86
8. theorem OAI.RyserCoveringCounterexample.Construction.placedExceptionalEdge_injective line 101
9. theorem OAI.RyserCoveringCounterexample.Construction.placedHypergraph_intersecting line 122