OAI/Combinatorics/RamseyFive/Geometry/UniformHighTail.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SharpRamseyFive.ScoreGeometry.eventually_high_original_tailline 15 - theorem
OAI.SharpRamseyFive.ScoreGeometry.eventually_local_trunc_scalar_retainedline 133 - theorem
OAI.SharpRamseyFive.ScoreGeometry.eventually_high_local_budget_retainedline 162 - theorem
OAI.SharpRamseyFive.ScoreGeometry.eventually_high_original_tail_retainedline 227