OAI/Geometry/IsometricImmersion/Caps/CapReflectionCalculus.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_coordinatePoint line 12
  2. theorem OAI.SmoothLocal.Flow.Reflection.reflectPoint_mem_capChartDomain line 17
  3. theorem OAI.SmoothLocal.Flow.Reflection.coordPartial_reflectedScalar line 25
  4. theorem OAI.SmoothLocal.Flow.Reflection.verticalJet_reflectedScalar line 36
  5. theorem OAI.SmoothLocal.Flow.Reflection.negOnePow_square line 61
  6. def OAI.SmoothLocal.Flow.Reflection.conjugateFlow line 65
  7. theorem OAI.SmoothLocal.Flow.Reflection.conjugateFlow_chart line 67
  8. theorem OAI.SmoothLocal.Flow.Reflection.conjugateFlow_start line 72
  9. theorem OAI.SmoothLocal.Flow.Reflection.conjugateFlow_chart_contDiffOn line 79
  10. theorem OAI.SmoothLocal.Flow.Reflection.conjugateFlow_displacement line 87
  11. theorem OAI.SmoothLocal.Flow.Reflection.conjugateFlow_ode line 97
  12. theorem OAI.SmoothLocal.Flow.Reflection.rectangleIntegral_reflectedScalar line 124
  13. theorem OAI.SmoothLocal.Flow.Reflection.reflectedScalar_gradient_square line 133
  14. theorem OAI.SmoothLocal.Flow.Reflection.rectangleGradient_reflectedScalar line 140