OAI/Combinatorics/HalvingLines/Curves.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Zoom.path_stays_inside line 12
2. lemma OAI.PlanarHalving.Zoom.inverse_bound line 26
3. lemma OAI.PlanarHalving.Zoom.inverse_near_id line 61
4. lemma OAI.PlanarHalving.Zoom.ray_image_leaves_ball line 76
5. lemma OAI.PlanarHalving.Zoom.line_parameter_levels line 107
6. lemma OAI.PlanarHalving.Zoom.line_parameter_curve line 148
7. lemma OAI.PlanarHalving.Zoom.intersects_level_graph line 186
8. lemma OAI.PlanarHalving.Zoom.bounded_parameter_tendsto line 210
9. lemma OAI.PlanarHalving.Zoom.parameter_curves_tendsto line 245
10. def OAI.PlanarHalving.Zoom.coneLevel line 269
11. lemma OAI.PlanarHalving.Zoom.coneLevel_apply line 273
12. lemma OAI.PlanarHalving.Zoom.norm_le_coneLevel line 276
13. lemma OAI.PlanarHalving.Zoom.coneLevel_strictMono line 290
14. lemma OAI.PlanarHalving.Zoom.coneLevel_chord line 304