OAI/Geometry/IsometricImmersion/Calculus/CoordinateJetNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.coordinateDirections line 12
  2. theorem OAI.SmoothLocal.Geometry.coordinateDirections_norm line 16
  3. theorem OAI.SmoothLocal.Geometry.iteratedCoordPartial_eq_jet line 25
  4. theorem OAI.SmoothLocal.Geometry.norm_iteratedCoordPartial_le_jet line 46
  5. theorem OAI.SmoothLocal.Geometry.coordinateBound_of_frechet_bounds line 56
  6. theorem OAI.SmoothLocal.Geometry.coordinateBound_five_of_frechet_eight line 63