OAI/Combinatorics/SharpRamsey/Planar/HeavyPlaneCurrent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.HeavyPlaneRestriction.center line 15
2. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.center_submodule line 21
3. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.restrict_ne_zero line 26
4. def OAI.SharpLogRamsey.HeavyPlaneRestriction.restrict line 36
5. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.restrict_eq_project line 42
6. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.incident_mk_left line 63
7. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.incident_mk_right line 72
8. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.restrict_incident_iff line 79
9. theorem OAI.SharpLogRamsey.HeavyPlaneRestriction.restrict_fiber_card line 91
10. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.center_restrict_zero line 119
11. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.center_incident line 127
12. lemma OAI.SharpLogRamsey.HeavyPlaneRestriction.sparse_noncentral line 134
13. theorem OAI.SharpLogRamsey.HeavyPlaneRestriction.sparse_restriction_class line 150