OAI/Combinatorics/HalvingLines/Rigidity.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarHalving.Zoom.LineControl line 12
2. lemma OAI.PlanarHalving.Zoom.moving_intersection_tendsto line 21
3. def OAI.PlanarHalving.Zoom.LineControl.of_monotone line 73
4. lemma OAI.PlanarHalving.Zoom.parallel_scalars_zero line 97
5. lemma OAI.PlanarHalving.Zoom.line_intersection_unique line 109
6. inductive OAI.PlanarHalving.Zoom.Foliation line 120
7. def OAI.PlanarHalving.Zoom.Foliation.direction line 126
8. lemma OAI.PlanarHalving.Zoom.Foliation.direction_ne_zero line 131
9. lemma OAI.PlanarHalving.Zoom.Foliation.transverse line 134
10. structure OAI.PlanarHalving.Zoom.FoliatedSequence line 138
11. def OAI.PlanarHalving.Zoom.FoliatedSequence.subseq line 145
12. def OAI.PlanarHalving.Zoom.FoliatedSequence.Good line 159
13. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.Good.subseq line 162
14. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_intersection line 166
15. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_rect line 181
16. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_diagonal_vertical line 189
17. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_diagonal_horizontal line 197
18. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_axis_swap line 205
19. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_axis_add line 211
20. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_axis_neg line 219
21. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_nat_axis line 226
22. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_int_axis line 236
23. lemma OAI.PlanarHalving.Zoom.FoliatedSequence.good_lattice line 247