OAI/Combinatorics/Crossing/VertexTruncation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Zarankiewicz.VertexTruncation line 10
  2. theorem OAI.Zarankiewicz.nonempty_vertexTruncation line 26
  3. def OAI.Zarankiewicz.VertexTruncation.pieces line 42
  4. def OAI.Zarankiewicz.VertexTruncation.vertices line 44
  5. def OAI.Zarankiewicz.VertexTruncation.startPort line 46
  6. def OAI.Zarankiewicz.VertexTruncation.endPort line 48
  7. theorem OAI.Zarankiewicz.VertexTruncation.pieces_pos line 50
  8. theorem OAI.Zarankiewicz.VertexTruncation.weak_short line 52
  9. def OAI.Zarankiewicz.VertexTruncation.path line 57
  10. theorem OAI.Zarankiewicz.VertexTruncation.path_injective line 60
  11. theorem OAI.Zarankiewicz.VertexTruncation.path_hasFiniteAffineCover line 64
  12. theorem OAI.Zarankiewicz.VertexTruncation.range_subset_edgeInterior line 67
  13. theorem OAI.Zarankiewicz.VertexTruncation.direction_ne_zero line 70