OAI/Combinatorics/SharpRamsey/Trees/ChronologicalOrder.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Selection.Law.exists_mass_pos_le_of_mean_leline 13 - lemma
OAI.SharpLogRamsey.Selection.reverse_incidence_countline 37 - theorem
OAI.SharpLogRamsey.Selection.auxiliary_cap_productline 45 - theorem
OAI.SharpLogRamsey.Selection.auxiliary_chronological_orderline 92