OAI/Geometry/IsometricImmersion/Darboux/ModelPrincipal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Model.modelPrincipalRemainderBound line 11
2. def OAI.SmoothLocal.Model.modelPrincipalRadius line 14
3. theorem OAI.SmoothLocal.Model.modelPrincipalRemainderBound_nonneg line 18
4. theorem OAI.SmoothLocal.Model.modelPrincipalRadius_pos line 23
5. theorem OAI.SmoothLocal.Model.modelPrincipal_derivative_remainder_bound line 32
6. theorem OAI.SmoothLocal.Model.modelPrincipal_radius_error line 57
7. theorem OAI.SmoothLocal.Model.model_full_principal_lower line 76