OAI/Combinatorics/Crossing/CrossingIncidence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Zarankiewicz.crossingCount_attainment line 11
  2. theorem OAI.Zarankiewicz.ordinaryCrossingNumber_le_count line 16
  3. theorem OAI.Zarankiewicz.crossing_incident_iff line 20
  4. theorem OAI.Zarankiewicz.crossing_two_edges line 36
  5. def OAI.Zarankiewicz.pairCrossings line 43
  6. theorem OAI.Zarankiewicz.pairCrossings_self line 47
  7. theorem OAI.Zarankiewicz.pairCrossings_comm line 51
  8. theorem OAI.Zarankiewicz.crossing_ordered_incidence line 57
  9. theorem OAI.Zarankiewicz.sum_pairCrossings_card line 81