OAI/Combinatorics/RamseyFive/Streams/SelectedExtraction.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpRamseyFive.SelectedTuple.mem_occurrences_iffline 12 - lemma
OAI.SharpRamseyFive.SelectedTuple.occurrences_transline 30 - theorem
OAI.SharpRamseyFive.SelectedTuple.retained_entropyline 37