OAI/Combinatorics/Ryser/Construction/PlacementIntersection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Construction.mem_range_placedPoint_of_incident_of_ne_placedLines line 9
2. theorem OAI.RyserCoveringCounterexample.Construction.eq_placedLine_of_incident_of_notMem_range line 32
3. theorem OAI.RyserCoveringCounterexample.Construction.eq_smallLine_of_incident_of_notMem_range line 42