OAI/Combinatorics/SharpRamsey/Planar/HeavyPlaneInput.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.HeavyPlaneRestriction.planeSupport line 23
2. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.planeSupport_image line 27
3. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.planeSupport_card line 42
4. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.planeSupport_incidence_le line 47
5. theorem OAI.SharpLogRamsey.HeavyPlaneRestriction.heavy_half line 59
6. theorem OAI.SharpLogRamsey.HeavyPlaneRestriction.heavy_reduction line 109