OAI/Geometry/IsometricImmersion/Caps/CapFlowUniqueness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Flow.cap_trajectory_mem_ball_of_displacement line 14
  2. theorem OAI.SmoothLocal.Flow.capChart_eqOn_of_same_ode line 30
  3. theorem OAI.SmoothLocal.Flow.capPullback_eventuallyEq_of_chart_eqOn line 59
  4. theorem OAI.SmoothLocal.Flow.capPullback_all_jets_eq_of_chart_eqOn line 66
  5. theorem OAI.SmoothLocal.Flow.capChart_images_eq_of_eqOn line 72
  6. theorem OAI.SmoothLocal.Flow.capPullback_square_rectangle_eq_of_chart_eqOn line 77
  7. theorem OAI.SmoothLocal.Flow.capPullback_gradient_rectangle_eq_of_chart_eqOn line 87