OAI/Combinatorics/SharpRamsey/Windows/IntegerExperiment.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpLogRamsey.Selection.Windows.integerBadline 25 - def
OAI.SharpLogRamsey.Selection.Windows.integerLiveline 31 - def
OAI.SharpLogRamsey.Selection.Windows.integerPopline 34 - def
OAI.SharpLogRamsey.Selection.Windows.integerTargetsline 43 - def
OAI.SharpLogRamsey.Selection.Windows.integerTreeline 48 - lemma
OAI.SharpLogRamsey.Selection.Windows.integerPopulation_sizeline 54 - lemma
OAI.SharpLogRamsey.Selection.Windows.integerPopulation_lengthline 66 - theorem
OAI.SharpLogRamsey.Selection.Windows.eventually_integer_experimentline 73