OAI/Combinatorics/HalvingLines/Intersections.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Zoom.intersects_parameter_graph line 12
2. lemma OAI.PlanarHalving.Zoom.eventual_arc_intersection line 43
3. lemma OAI.PlanarHalving.Zoom.level_forces_nonzero line 102
4. def OAI.PlanarHalving.Zoom.DirectionalLimit line 132
5. lemma OAI.PlanarHalving.Zoom.controlled_line_arcs line 140
6. lemma OAI.PlanarHalving.Zoom.moving_line_arcs_tendsto line 184
7. lemma OAI.PlanarHalving.Zoom.line_intersection_tendsto line 229
8. def OAI.PlanarHalving.Zoom.detPair line 310
9. lemma OAI.PlanarHalving.Zoom.plane_span line 312
10. lemma OAI.PlanarHalving.Zoom.transverse_covector line 324
11. lemma OAI.PlanarHalving.Zoom.detPair_smul_right line 354