OAI/Combinatorics/Crossing/ChordPairing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.orderSign line 8
2. def OAI.Zarankiewicz.chordEndpointPairing line 10
3. theorem OAI.Zarankiewicz.orderSign_swap line 13
4. theorem OAI.Zarankiewicz.chordEndpointPairing_reverse_left line 17
5. theorem OAI.Zarankiewicz.chordEndpointPairing_swap line 22
6. theorem OAI.Zarankiewicz.circle_chords_separated line 28
7. theorem OAI.Zarankiewicz.circle_chords_nested line 34
8. theorem OAI.Zarankiewicz.circle_chord_pairing_ordered line 45