OAI/Geometry/IsometricImmersion/Taylor/TopChainExtraction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.HighEquation.ChainWord.prepend_single line 12
  2. theorem OAI.SmoothLocal.HighEquation.ChainWord.bump_single line 15
  3. theorem OAI.SmoothLocal.HighEquation.ChainWord.prepend_pair line 23
  4. theorem OAI.SmoothLocal.HighEquation.ChainWord.bump_pair_zero line 26
  5. theorem OAI.SmoothLocal.HighEquation.ChainWord.bump_pair_one line 33
  6. theorem OAI.SmoothLocal.HighEquation.chainTerm_single_eq line 42
  7. theorem OAI.SmoothLocal.HighEquation.chainTerm_pair_eq line 49
  8. theorem OAI.SmoothLocal.HighEquation.chainTerm_triple_eq line 56
  9. theorem OAI.SmoothLocal.HighEquation.chainTerm_pair_symm line 64
  10. theorem OAI.SmoothLocal.HighEquation.chainTerm_single_hasDerivAt line 73
  11. theorem OAI.SmoothLocal.HighEquation.chainTerm_pair_hasDerivAt line 85
  12. theorem OAI.SmoothLocal.HighEquation.top_chain_three line 98
  13. theorem OAI.SmoothLocal.HighEquation.top_chain_expansion line 124
  14. theorem OAI.SmoothLocal.HighEquation.actualP_top_chain_expansion line 161