OAI/Combinatorics/HalvingLines/Foliations.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Zoom.equiv_opNorm_pos line 11
2. def OAI.PlanarHalving.Zoom.normalizedLinear line 21
3. lemma OAI.PlanarHalving.Zoom.normalizedLinear_norm line 24
4. lemma OAI.PlanarHalving.Zoom.unit_conorm_all line 27
5. lemma OAI.PlanarHalving.Zoom.normalizedLinear_subsequence line 41
6. lemma OAI.PlanarHalving.Zoom.uniform_apply_linear_limit line 66
7. lemma OAI.PlanarHalving.Zoom.affineZoom_symm_apply line 100
8. lemma OAI.PlanarHalving.Zoom.common_inverse_identity line 105
9. lemma OAI.PlanarHalving.Zoom.uniform_common_inverse_limit line 116
10. lemma OAI.PlanarHalving.Zoom.common_frame_condition line 153
11. def OAI.PlanarHalving.Zoom.RadialCompare line 182
12. lemma OAI.PlanarHalving.Zoom.uniform_radial_compare line 188
13. lemma OAI.PlanarHalving.Zoom.radial_compare_of_zoom line 239
14. lemma OAI.PlanarHalving.Directions.allowed_closed line 266
15. def OAI.PlanarHalving.Zoom.FrameCondition line 290
16. lemma OAI.PlanarHalving.Zoom.exists_frameCondition line 300
17. lemma OAI.PlanarHalving.Zoom.common_limit_bounds line 307
18. lemma OAI.PlanarHalving.RankLimits.actual_common_inverse_limit line 340