OAI/Geometry/IsometricImmersion/Calculus/CoordinateJetBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.CoordinateBound line 11
  2. theorem OAI.SmoothLocal.Geometry.CoordinateBound.mono line 16
  3. theorem OAI.SmoothLocal.Geometry.CoordinateBound.iterated_append line 20
  4. theorem OAI.SmoothLocal.Geometry.CoordinateBound.partial_bound line 26
  5. theorem OAI.SmoothLocal.Geometry.CoordinateBound.iterated_add line 34
  6. theorem OAI.SmoothLocal.Geometry.CoordinateBound.iterated_sub line 52
  7. theorem OAI.SmoothLocal.Geometry.CoordinateBound.iterated_const_mul line 70
  8. theorem OAI.SmoothLocal.Geometry.CoordinateBound.add line 88
  9. theorem OAI.SmoothLocal.Geometry.CoordinateBound.sub line 96
  10. theorem OAI.SmoothLocal.Geometry.CoordinateBound.const_mul line 104
  11. theorem OAI.SmoothLocal.Geometry.CoordinateBound.neg line 111
  12. theorem OAI.SmoothLocal.Geometry.CoordinateBound.abs_add_bound line 116
  13. theorem OAI.SmoothLocal.Geometry.CoordinateBound.mul_through_three line 119