OAI/Combinatorics/RamseyFive/Bounds/DensityUpper.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.ProjectiveIncidence.density_upperline 13 - theorem
OAI.SharpRamseyFive.ProjectiveIncidence.incidence_rectangle_sqrtline 22 - theorem
OAI.SharpRamseyFive.ProjectiveIncidence.incidence_rectangle_logline 54