OAI/Geometry/CylinderCovering/Rational/GlobalQuantitative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SlopeRational.global_displacement_lipschitz line 12
2. theorem OAI.SlopeRational.global_tiltedMap_metric_bounds line 25
3. theorem OAI.SlopeRational.global_tiltedMap_uniform_metric_bounds line 43
4. theorem OAI.SlopeRational.global_wall_factors_pos line 55
5. theorem OAI.SlopeRational.global_wall_zero_iff line 76
6. theorem OAI.SlopeRational.global_wall_pos_iff line 88
7. theorem OAI.SlopeRational.global_wedge_homeomorphism line 99
8. theorem OAI.SlopeRational.rational_global_inverse_uniform line 132