OAI/Combinatorics/Crossing/DiskPassage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Zarankiewicz.DiskPassage line 9
2. theorem OAI.Zarankiewicz.nonempty_diskPassage line 22
3. theorem OAI.Zarankiewicz.DiskPassage.enter_lt_leave line 50
4. theorem OAI.Zarankiewicz.DiskPassage.enter_at_source line 55
5. theorem OAI.Zarankiewicz.DiskPassage.leave_at_target line 60
6. theorem OAI.Zarankiewicz.DiskPassage.enter_pos_of_source_outside line 65
7. theorem OAI.Zarankiewicz.DiskPassage.leave_lt_one_of_target_outside line 73