OAI/Combinatorics/HalvingLines/LocalZoom.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarHalving.Zoom.columnMap line 10
2. lemma OAI.PlanarHalving.Zoom.columnMap_apply line 13
3. def OAI.PlanarHalving.Zoom.columnEquiv line 15
4. lemma OAI.PlanarHalving.Zoom.columnEquiv_apply line 30
5. lemma OAI.PlanarHalving.Zoom.detPair_smul line 33
6. lemma OAI.PlanarHalving.Zoom.three_frame line 37
7. lemma OAI.PlanarHalving.Zoom.slope_frame line 61
8. def OAI.PlanarHalving.Zoom.affineHomeomorph line 85
9. lemma OAI.PlanarHalving.Zoom.affineHomeomorph_apply line 97
10. lemma OAI.PlanarHalving.Zoom.affineHomeomorph_symm_apply line 100
11. def OAI.PlanarHalving.Zoom.affineZoom line 103
12. lemma OAI.PlanarHalving.Zoom.affineZoom_apply line 109
13. lemma OAI.PlanarHalving.Zoom.affineZoom_source line 113
14. lemma OAI.PlanarHalving.Zoom.affineZoom_target line 120
15. lemma OAI.PlanarHalving.Zoom.affineZoom_zero line 124
16. lemma OAI.PlanarHalving.Zoom.affineZoom_exhaust line 130
17. lemma OAI.PlanarHalving.Zoom.affineZoom_normalizing_scale line 151
18. lemma OAI.PlanarHalving.RankLimits.affine_rank_monotone line 181
19. lemma OAI.PlanarHalving.RankLimits.affine_rank_direction line 213
20. lemma OAI.PlanarHalving.RankLimits.actual_zoom_compactness line 268
21. lemma OAI.PlanarHalving.RankLimits.timeSlope_eventually_lt line 330
22. def OAI.PlanarHalving.RankLimits.foliationTriple line 343
23. lemma OAI.PlanarHalving.RankLimits.positive_slope_frames line 348
24. lemma OAI.PlanarHalving.RankLimits.singleton_target_frame line 362