OAI/Geometry/NilpotentCharts/SmoothCalculus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth local inverses, parameter derivatives and vector parts of closed additive groups.

  1. theorem OAI.RawSliceInverse.exists_smooth_local_inverse line 17
  2. def OAI.RawParameterDerivative.D line 55
  3. lemma OAI.RawParameterDerivative.contDiff_parameter_derivative line 57
  4. def OAI.RawParameterDerivativeGeneral.D line 102
  5. lemma OAI.RawParameterDerivativeGeneral.contMDiff_parameter_derivative line 104
  6. lemma OAI.RawSmoothInverse.contMDiff_inverse line 156
  7. lemma OAI.RawClosedAddGroup.deriv_mem line 207
  8. def OAI.RawClosedAddGroup.vectorPart line 224
  9. lemma OAI.RawClosedAddGroup.vectorPart_le line 230
  10. lemma OAI.RawClosedAddGroup.deriv_mem_vectorPart line 234
  11. lemma OAI.RawClosedAddGroup.curve_mem_vectorPart line 246