OAI/Geometry/SurfaceImmersion/Whitney/TransverseRuledSurface.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The ruled map retaining the original value and transverse first jet along the full joining axis.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.axisValue line 15
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.axisTransverse line 16
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseRuling line 18
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.axisValue_smooth line 21
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.axisTransverse_smooth line 23
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseRuling_smooth line 26
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseRuling_axis line 31
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.axisValue_deriv line 35
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.axisTransverse_deriv line 40
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseRuling_fderiv line 48
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseRuling_first_jet line 62