OAI/Geometry/PolarProducts/SmoothPaths.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothPaths.applyField line 22
  2. theorem OAI.SmoothPaths.applyField_apply line 35
  3. def OAI.SmoothPaths.applyFieldCLM line 38
  4. theorem OAI.SmoothPaths.applyFieldCLM_apply line 57
  5. def OAI.SmoothPaths.superpose line 60
  6. theorem OAI.SmoothPaths.superpose_apply line 64
  7. theorem OAI.SmoothPaths.continuous_superpose line 68
  8. theorem OAI.SmoothPaths.hasFDerivAt_superpose line 72
  9. theorem OAI.SmoothPaths.contDiff_superpose_nat line 111
  10. theorem OAI.SmoothPaths.contDiff_superpose line 125