OAI/Combinatorics/Crossing/AxisCrossingOrder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.positive_scaled_eq_sign line 9
2. theorem OAI.Zarankiewicz.axis_meeting_abs_order line 16
3. theorem OAI.Zarankiewicz.BalancedAxisRealization.meeting_same_rays line 36
4. theorem OAI.Zarankiewicz.BalancedAxisRealization.meeting_reverse_horizontal_order line 55
5. theorem OAI.Zarankiewicz.BalancedAxisRealization.meeting_balanced_pairs line 69