OAI/Combinatorics/Crossing/DrawingDefinition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Zarankiewicz.Plane line 17

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:20 (same declaration text).

2. abbrev OAI.Zarankiewicz.BipartiteVertex line 18

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:21 (same declaration text).

3. abbrev OAI.Zarankiewicz.BipartiteEdge line 19

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:22 (same declaration text).

4. structure OAI.Zarankiewicz.ContinuousDrawing line 21

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:24 (same declaration text).

5. def OAI.Zarankiewicz.edgeInterior line 29

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:32 (same declaration text).

6. def OAI.Zarankiewicz.ProperCrossing line 32

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:35 (same declaration text).

7. def OAI.Zarankiewicz.crossingPoints line 38

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:41 (same declaration text).

8. structure OAI.Zarankiewicz.AdmissibleDrawing line 41

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:44 (same declaration text).

9. def OAI.Zarankiewicz.crossingCount line 50

   Also declared: ComparatorChallenges/BipartiteCrossing.lean:53 (same declaration text).

10. def OAI.Zarankiewicz.ordinaryCrossingNumber line 52
11. def OAI.Zarankiewicz.MainTarget line 54

    Also declared: ComparatorChallenges/BipartiteCrossing.lean:55 (same declaration text).

12. theorem OAI.Zarankiewicz.crossing_mem_of_interiors line 59