OAI/Geometry/IsometricImmersion/Darboux/QFirstJetFunctions.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Pulse.QFirstInput line 13
  2. def OAI.SmoothLocal.Pulse.qFirstDet line 15
  3. def OAI.SmoothLocal.Pulse.qFirstConnection line 16
  4. def OAI.SmoothLocal.Pulse.qFirstXX line 18
  5. def OAI.SmoothLocal.Pulse.qFirstMixed line 19
  6. def OAI.SmoothLocal.Pulse.qFirstEnergy line 20
  7. def OAI.SmoothLocal.Pulse.qFirstDensityFactor line 24
  8. def OAI.SmoothLocal.Pulse.qFirstLower line 26
  9. def OAI.SmoothLocal.Pulse.qFirstBundle line 29
  10. theorem OAI.SmoothLocal.Pulse.qFirstDet_bundle line 32
  11. theorem OAI.SmoothLocal.Pulse.qFirstConnection_bundle line 34
  12. theorem OAI.SmoothLocal.Pulse.qFirstXX_bundle line 36
  13. theorem OAI.SmoothLocal.Pulse.qFirstDensityFactor_bundle line 38
  14. theorem OAI.SmoothLocal.Pulse.qFirstLower_bundle line 40
  15. theorem OAI.SmoothLocal.Pulse.qFirstBundle_distance line 43
  16. def OAI.SmoothLocal.Pulse.qFirstBase line 48
  17. def OAI.SmoothLocal.Pulse.qFirstDomain line 49
  18. def OAI.SmoothLocal.Pulse.qFirstBaseTube line 50
  19. def OAI.SmoothLocal.Pulse.qFirstTube line 52
  20. theorem OAI.SmoothLocal.Pulse.qFirstDet_contDiff line 55
  21. theorem OAI.SmoothLocal.Pulse.qFirstBase_isOpen line 60
  22. theorem OAI.SmoothLocal.Pulse.qFirstConnection_contDiffAt line 63
  23. theorem OAI.SmoothLocal.Pulse.qFirstXX_contDiffOn line 78
  24. theorem OAI.SmoothLocal.Pulse.qFirstDomain_isOpen line 83
  25. theorem OAI.SmoothLocal.Pulse.qFirstEnergy_contDiff line 87
  26. theorem OAI.SmoothLocal.Pulse.qFirstDensityFactor_contDiffOn line 100
  27. theorem OAI.SmoothLocal.Pulse.qFirstLower_contDiffOn line 107
  28. theorem OAI.SmoothLocal.Pulse.qFirstBaseTube_isCompact line 115
  29. theorem OAI.SmoothLocal.Pulse.qFirstBaseTube_subset_base line 119
  30. theorem OAI.SmoothLocal.Pulse.qFirstTube_isCompact line 124
  31. theorem OAI.SmoothLocal.Pulse.qFirstTube_subset_domain line 133
  32. theorem OAI.SmoothLocal.Pulse.qFirstXX_fderiv_bound line 142
  33. theorem OAI.SmoothLocal.Pulse.qFirstTube_fderiv_bound line 150