OAI/Combinatorics/RamseyFive/Streams/SelectedLength.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.SelectedTuple.SelectedStream.length_le_sourceline 17 - theorem
OAI.SharpRamseyFive.SelectedTuple.eventually_high_prepared_impossibleline 29