OAI/Combinatorics/Crossing/BalancedAxisIntervals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Zarankiewicz.axisIntervalLo line 8
2. def OAI.Zarankiewicz.axisIntervalHi line 9
3. theorem OAI.Zarankiewicz.axisInterval_nonempty line 11
4. theorem OAI.Zarankiewicz.axisInterval_abs_bounds line 15
5. theorem OAI.Zarankiewicz.axisInterval_sign line 27
6. theorem OAI.Zarankiewicz.axisInterval_ne_zero line 39
7. theorem OAI.Zarankiewicz.axisInterval_abs_strictMono line 47
8. theorem OAI.Zarankiewicz.axisInterval_injective line 56