OAI/Combinatorics/Crossing/VertexOrderDetector.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.leftNode line 11
2. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.leftNode_injective line 13
3. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.leftOrder line 18
4. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.leftHalfOrder_eq_halfOrder line 20
5. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.diagonal_detector_isUnit line 28
6. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.offDiagonal_detector line 35
7. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.additive_detector_relation line 40