OAI/Geometry/IsometricImmersion/Darboux/QSpatialRestriction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.HighEquation.QSpatialState line 13
  2. def OAI.SmoothLocal.HighEquation.qSpatialAxis line 15
  3. def OAI.SmoothLocal.HighEquation.qSpatialIndex line 16
  4. def OAI.SmoothLocal.HighEquation.qSpatialLinear line 18
  5. def OAI.SmoothLocal.HighEquation.qSpatialCLM line 23
  6. def OAI.SmoothLocal.HighEquation.qFixedTimeState line 26
  7. def OAI.SmoothLocal.HighEquation.qSpatialProjection line 29
  8. def OAI.SmoothLocal.HighEquation.qFixedTimeQ line 31
  9. def OAI.SmoothLocal.HighEquation.qFixedTimeDomain line 34
  10. theorem OAI.SmoothLocal.HighEquation.qSpatialAxis_index line 37
  11. theorem OAI.SmoothLocal.HighEquation.qSpatialCLM_single line 40
  12. theorem OAI.SmoothLocal.HighEquation.qFixedTimeState_projection line 46
  13. theorem OAI.SmoothLocal.HighEquation.qFixedTimeState_contDiff line 52
  14. theorem OAI.SmoothLocal.HighEquation.qFixedTimeDomain_isOpen line 55
  15. theorem OAI.SmoothLocal.HighEquation.qFixedTimeQ_contDiffOn line 60
  16. theorem OAI.SmoothLocal.HighEquation.qFixedTimeQ_iteratedFDeriv line 66
  17. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainCoefficient_eq_fixedTime line 87
  18. theorem OAI.SmoothLocal.HighEquation.qCoordinateChainCoefficient_abs_le_fixedTime_derivative line 108