OAI/Combinatorics/SharpRamsey/Selection/SourceGridShape.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.SourceScales.log_grid_bound line 13
2. theorem OAI.SharpLogRamsey.SourceScales.eventually_grid_shape line 22
3. lemma OAI.SharpLogRamsey.SourceScales.support_le_projective_power line 46