OAI/Geometry/CylinderCovering/Convexity/ThresholdInversion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.ThresholdInversion.inverse_distance_bound line 14
2. theorem OAI.CylinderCovering.ThresholdInversion.inverse_displacement_error line 26
3. theorem OAI.CylinderCovering.ThresholdInversion.inverse_unique line 40
4. theorem OAI.CylinderCovering.ThresholdInversion.existsUnique_inverse_on line 48
5. theorem OAI.CylinderCovering.ThresholdInversion.inverse_height_strict line 78
6. theorem OAI.CylinderCovering.ThresholdInversion.box_iteration_mapsTo line 109
7. theorem OAI.CylinderCovering.ThresholdInversion.existsUnique_inverse_on_box line 122
8. theorem OAI.CylinderCovering.ThresholdInversion.existsUnique_inverse_on_box_smul line 146
9. theorem OAI.CylinderCovering.ThresholdInversion.exists_small_tilt line 177
10. theorem OAI.CylinderCovering.ThresholdInversion.inverse_coordinate_strict line 191