OAI/Combinatorics/Crossing/PolygonalNormalization.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.alternatingPath_hasFiniteAffineCoverline 9 - theorem
OAI.Zarankiewicz.PolygonalExterior.middlePath_hasFiniteAffineCoverline 19 - theorem
OAI.Zarankiewicz.PolygonalExterior.assembledEdge_hasFiniteAffineCoverline 24 - theorem
OAI.Zarankiewicz.finite_intersection_normalizationline 35 - theorem
OAI.Zarankiewicz.polygonal_normalizationline 44