OAI/Geometry/IsometricImmersion/Calculus/ClosedSquareJetBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Geometry.modelSquare_closure_interior line 16
2. theorem OAI.SmoothLocal.Geometry.CoordinateBound.restrict_domain line 22
3. theorem OAI.SmoothLocal.Geometry.CoordinateBound.of_modelSquare_interior line 26
4. theorem OAI.SmoothLocal.Geometry.inverseMetric_coordinate_bound_closed_square line 39
5. theorem OAI.SmoothLocal.Geometry.covHessian_coordinate_bound_closed_square line 53
6. theorem OAI.SmoothLocal.Geometry.exists_open_quotient_domain_with_closed_low_bounds line 68