OAI/Combinatorics/SharpRamsey/Reciprocal/AuxiliaryFamilies.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SharpLogRamsey.Selection.Law.pi_coordinate_sumline 14 - lemma
OAI.SharpLogRamsey.Selection.Law.independent_coordinates_sumline 37 - def
OAI.SharpLogRamsey.Selection.AuxiliarySupport.familyLawline 51 - lemma
OAI.SharpLogRamsey.Selection.AuxiliarySupport.familyLaw_supportline 56 - theorem
OAI.SharpLogRamsey.Selection.AuxiliarySupport.familyLaw_incidenceline 73 - lemma
OAI.SharpLogRamsey.Selection.Law.history_observable_sumline 94 - lemma
OAI.SharpLogRamsey.Selection.Law.withKernel_observable_sumline 103