OAI/Combinatorics/Crossing/GeneralSpokeAveraging.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Zarankiewicz.small_perturbation_injectiveline 9 - theorem
OAI.Zarankiewicz.fixed_node_ne_small_perturbationline 22 - theorem
OAI.Zarankiewicz.local_spoke_straddling_averageline 34