OAI/Geometry/IsometricImmersion/Darboux/TransverseCoefficient.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.flowRho line 12
  2. def OAI.SmoothLocal.Geometry.flowSigma line 14
  3. def OAI.SmoothLocal.Geometry.transverseA line 16
  4. def OAI.SmoothLocal.Geometry.transversePartial line 19
  5. def OAI.SmoothLocal.Geometry.transverseC line 22
  6. def OAI.SmoothLocal.Geometry.transverseRemainder line 29
  7. theorem OAI.SmoothLocal.Geometry.flowRho_contDiffOn line 37
  8. theorem OAI.SmoothLocal.Geometry.flowSigma_contDiffOn line 41
  9. theorem OAI.SmoothLocal.Geometry.transverseA_contDiffOn line 45
  10. theorem OAI.SmoothLocal.Geometry.transverseA_partial_y line 53
  11. theorem OAI.SmoothLocal.Geometry.transverseA_partial_s line 79
  12. theorem OAI.SmoothLocal.Geometry.transverseC_eq line 92
  13. theorem OAI.SmoothLocal.Geometry.transversePartialA_contDiffOn line 113
  14. theorem OAI.SmoothLocal.Geometry.transverseRemainder_contDiffOn line 122
  15. theorem OAI.SmoothLocal.Geometry.transverseRemainder_bounded_on_compact line 142
  16. theorem OAI.SmoothLocal.Geometry.transverseRemainder_bound line 159