OAI/Combinatorics/Crossing/MarkedCurveDisks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.closedRoundDisk_mono line 8
2. theorem OAI.Zarankiewicz.finite_curve_mark_isolation line 15