OAI/Combinatorics/SharpRamsey/Learning/PreparedGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.GreedyPreparation.own_empty_or_index line 14
2. def OAI.SharpLogRamsey.PreparedGeometry.badHyperplanes line 40
3. lemma OAI.SharpLogRamsey.PreparedGeometry.not_bad line 46
4. lemma OAI.SharpLogRamsey.PreparedGeometry.cell_sum_le line 63
5. lemma OAI.SharpLogRamsey.PreparedGeometry.pencil_exception_count line 69
6. theorem OAI.SharpLogRamsey.PreparedGeometry.regular_preparation line 79