OAI/Geometry/SurfaceImmersion/Primitive/CircularBoundaryTangencies.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Derivatives along the explicit circle equal evaluation of the actual phase covector on its nonzero angular tangent. Compact parameter finiteness therefore gives finiteness of the genuine surface tangency set.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularAngularTangent line 16
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularAngularTangent_param line 18
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularPhaseDerivative line 22
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularPhaseDerivative_eq_deriv line 27
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularPhaseTangencies line 48
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularPhaseTangencies_finite line 51