OAI/Combinatorics/SharpRamsey/Selection/FreshFamilies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.PublicTables.piLaw line 13
2. abbrev OAI.SharpLogRamsey.PublicTables.Outside line 18
3. def OAI.SharpLogRamsey.PublicTables.outside line 20
4. def OAI.SharpLogRamsey.PublicTables.outsideLaw line 22
5. lemma OAI.SharpLogRamsey.PublicTables.family_mass_split line 25
6. theorem OAI.SharpLogRamsey.PublicTables.family_integral line 35
7. theorem OAI.SharpLogRamsey.PublicTables.ready_family_bound line 55
8. theorem OAI.SharpLogRamsey.PublicTables.predictable_budget line 69
9. theorem OAI.SharpLogRamsey.PublicTables.exists_fixed_family line 103