OAI/Combinatorics/HalvingLines/Enhancement.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarHalving.Enhancement.Space line 11
2. def OAI.PlanarHalving.Enhancement.label line 12
3. def OAI.PlanarHalving.Enhancement.points line 14
4. def OAI.PlanarHalving.Enhancement.vertices line 16
5. def OAI.PlanarHalving.Enhancement.edges line 18
6. lemma OAI.PlanarHalving.Enhancement.points_map line 21
7. lemma OAI.PlanarHalving.Enhancement.vertices_map line 24
8. lemma OAI.PlanarHalving.Enhancement.edges_map line 28
9. lemma OAI.PlanarHalving.Enhancement.points_mass line 33
10. lemma OAI.PlanarHalving.Enhancement.vertices_mass line 36
11. lemma OAI.PlanarHalving.Enhancement.edges_mass line 39
12. inductive OAI.PlanarHalving.Enhancement.Index line 44
13. def OAI.PlanarHalving.Enhancement.measures line 50
14. def OAI.PlanarHalving.Enhancement.old line 54
15. lemma OAI.PlanarHalving.Enhancement.measures_mass_le line 59
16. theorem OAI.PlanarHalving.Enhancement.subsequence line 70
17. lemma OAI.PlanarHalving.Enhancement.vertices_le_points line 95
18. lemma OAI.PlanarHalving.Enhancement.local_cubic line 107
19. lemma OAI.PlanarHalving.Spatial.support_lift_restrict line 150
20. lemma OAI.PlanarHalving.Spatial.support_lift_disk line 158
21. lemma OAI.PlanarHalving.Spatial.unit_sqNorm_coordinate_bounds line 205
22. lemma OAI.PlanarHalving.Spatial.unit_sqNorm_norm line 214
23. lemma OAI.PlanarHalving.Spatial.transverse_decomposition line 218
24. lemma OAI.PlanarHalving.Spatial.bounded_strip_cover line 224
25. lemma OAI.PlanarHalving.Spatial.strip_bound_of_disk line 325
26. lemma OAI.PlanarHalving.Spatial.line_null_of_disk line 347