OAI/Combinatorics/Crossing/EndpointFlagPairing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Zarankiewicz.IncidentFlag line 9
  2. def OAI.Zarankiewicz.dartSourceFlag line 11
  3. def OAI.Zarankiewicz.dartTargetFlag line 14
  4. theorem OAI.Zarankiewicz.incidentCast_refl line 17
  5. theorem OAI.Zarankiewicz.incidentFlag_cast line 20
  6. theorem OAI.Zarankiewicz.dartPassageNext_flag line 25
  7. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.flagPairing line 34
  8. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.vertexChordPairing_flags line 37
  9. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.passagePairing_flags line 48
  10. def OAI.Zarankiewicz.TruncatedSpokeCoordinates.edgeEndpointPairing line 58
  11. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.flagPairing_source_target line 62
  12. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.flagPairing_target_source line 66
  13. theorem OAI.Zarankiewicz.TruncatedSpokeCoordinates.dart_endpoint_pairing line 70