OAI/Geometry/IsometricImmersion/Calculus/FinitePrimitive.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Flow.pairRectangle line 12
  2. def OAI.SmoothLocal.Flow.pairPrimitive line 14
  3. def OAI.SmoothLocal.Flow.pairPartialY line 17
  4. def OAI.SmoothLocal.Flow.pairCompactFamily line 20
  5. theorem OAI.SmoothLocal.Flow.pairRectangle_isOpen line 23
  6. theorem OAI.SmoothLocal.Flow.exists_compact_time_interval line 26
  7. theorem OAI.SmoothLocal.Flow.pairCompactFamily_joint_continuous line 35
  8. theorem OAI.SmoothLocal.Flow.pairCompactFamily_continuousOn line 43
  9. theorem OAI.SmoothLocal.Flow.pairCompactFamily_apply line 48
  10. theorem OAI.SmoothLocal.Flow.pairPrimitive_eq_clamped line 58
  11. theorem OAI.SmoothLocal.Flow.pairPrimitive_continuousOn line 71
  12. theorem OAI.SmoothLocal.Flow.pairPartialY_contDiffOn line 87
  13. theorem OAI.SmoothLocal.Flow.pairCompactFamily_hasDerivAt line 94
  14. theorem OAI.SmoothLocal.Flow.pairPrimitive_hasDerivAt_y line 115
  15. theorem OAI.SmoothLocal.Flow.pairPrimitive_hasDerivAt_x line 130
  16. theorem OAI.SmoothLocal.Flow.pairPrimitive_contDiffOn_nat line 142