OAI/Geometry/IsometricImmersion/Taylor/ChainTermDerivative.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SmoothLocal.HighEquation.ChainWord line 14
  2. def OAI.SmoothLocal.HighEquation.ChainWord.prepend line 18
  3. def OAI.SmoothLocal.HighEquation.ChainWord.bump line 21
  4. def OAI.SmoothLocal.HighEquation.ChainWord.total line 24
  5. def OAI.SmoothLocal.HighEquation.ChainWord.Positive line 26
  6. def OAI.SmoothLocal.HighEquation.ChainWord.Bounded line 28
  7. def OAI.SmoothLocal.HighEquation.chainTerm line 30
  8. theorem OAI.SmoothLocal.HighEquation.iteratedDeriv_contDiffAt_infty line 34
  9. theorem OAI.SmoothLocal.HighEquation.iteratedDeriv_hasDerivAt_infty line 45
  10. theorem OAI.SmoothLocal.HighEquation.chainTerm_hasDerivAt line 52
  11. theorem OAI.SmoothLocal.HighEquation.ChainWord.prepend_positive line 84
  12. theorem OAI.SmoothLocal.HighEquation.ChainWord.bump_positive line 91
  13. theorem OAI.SmoothLocal.HighEquation.ChainWord.prepend_total line 100
  14. theorem OAI.SmoothLocal.HighEquation.ChainWord.bump_total line 104
  15. theorem OAI.SmoothLocal.HighEquation.ChainWord.prepend_bounded line 116
  16. theorem OAI.SmoothLocal.HighEquation.ChainWord.bump_bounded line 123
  17. theorem OAI.SmoothLocal.HighEquation.actualP_chainTerm_hasDerivAt line 133