OAI/Combinatorics/HalvingLines/ThinStrips.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Spatial.isOpenMap_encode line 11
2. lemma OAI.PlanarHalving.Spatial.isOpen_square line 16
3. lemma OAI.PlanarHalving.Spatial.continuous_dot line 21
4. def OAI.PlanarHalving.Spatial.awayStrips line 24
5. lemma OAI.PlanarHalving.Spatial.isOpen_awayStrips line 27
6. lemma OAI.PlanarHalving.Spatial.awayStrips_stable line 34
7. lemma OAI.PlanarHalving.Spatial.awayStrips_antitone line 73
8. lemma OAI.PlanarHalving.Spatial.awayStrips_iUnion line 77
9. lemma OAI.PlanarHalving.Spatial.moving_strips_limit line 93
10. lemma OAI.PlanarHalving.Spatial.limiting_activity_bound line 137
11. def OAI.PlanarHalving.Boundary.batchRange line 205
12. lemma OAI.PlanarHalving.Boundary.sum_batchRange line 208
13. lemma OAI.PlanarHalving.Boundary.sum_disjoint_ranges line 228
14. lemma OAI.PlanarHalving.Boundary.parameter_telescope line 236
15. lemma OAI.PlanarHalving.Boundary.parameter_range_sum line 243
16. lemma OAI.PlanarHalving.Boundary.parameter_budget line 249
17. lemma OAI.PlanarHalving.TimeWindows.cuts_of_subset line 265
18. lemma OAI.PlanarHalving.TimeWindows.relative_end_le line 270
19. lemma OAI.PlanarHalving.Batches.System.vertices_eq_of_marks line 282
20. lemma OAI.PlanarHalving.Batches.System.relative_vertices line 288
21. abbrev OAI.PlanarHalving.Boundary.CompactParams line 307
22. lemma OAI.PlanarHalving.Boundary.params_subsequence line 309
23. lemma OAI.PlanarHalving.Boundary.finite_budget_limit line 334
24. lemma OAI.PlanarHalving.Batches.System.vertices_changes line 346
25. lemma OAI.PlanarHalving.Batches.System.tokenState_image line 359
26. def OAI.PlanarHalving.Batches.System.boundaryCount line 372
27. lemma OAI.PlanarHalving.Batches.System.boundary_budget line 378
28. lemma OAI.PlanarHalving.Batches.System.window_boundary line 388
29. abbrev OAI.PlanarHalving.TimeWindows.Subwindow line 455
30. lemma OAI.PlanarHalving.TimeWindows.relative_range_disjoint line 457