OAI/Combinatorics/RamseyFive/Entropy/EventuallyHighPolyCost.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SharpRamseyFive.ScoreGeometry.eventually_high_poly_costline 11 - theorem
OAI.SharpRamseyFive.ScoreGeometry.eventually_high_pair_costline 51