OAI/Combinatorics/SharpRamsey/Planar/HeavyPlanePublic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpLogRamsey.HeavyPlaneRestriction.HeavyHeaders line 28
2. abbrev OAI.SharpLogRamsey.HeavyPlaneRestriction.headerPlane line 33
3. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.header_rank line 35
4. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.header_codim line 37
5. def OAI.SharpLogRamsey.HeavyPlaneRestriction.headerDomain line 39
6. def OAI.SharpLogRamsey.HeavyPlaneRestriction.HeaderValid line 44
7. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.header_card line 53
8. theorem OAI.SharpLogRamsey.HeavyPlaneRestriction.heavy_families line 63
9. theorem OAI.SharpLogRamsey.HeavyPlaneRestriction.public_heavy_cover line 160