OAI/Combinatorics/SharpRamsey/Selection/OriginalFamilies.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpLogRamsey.ActualPivot.OriginalChoice line 25
2. lemma OAI.SharpLogRamsey.ActualPivot.originalChoice_size line 29
3. def OAI.SharpLogRamsey.ActualPivot.originalFamily line 35
4. theorem OAI.SharpLogRamsey.ActualPivot.originalFamily_density line 57
5. lemma OAI.SharpLogRamsey.ActualPivot.firstTargetDensity_mean line 73
6. lemma OAI.SharpLogRamsey.ActualPivot.secondTargetDensity_mean line 86
7. theorem OAI.SharpLogRamsey.ActualPivot.originalFamily_first_target line 99
8. theorem OAI.SharpLogRamsey.ActualPivot.originalFamily_second_target line 130