OAI/Geometry/SurfaceImmersion/Whitney/CrosscapSecondDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact second derivative of the standard crosscap and the chain rule in a kernel direction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.standardCrosscapDerivative_zero_apply line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.standardCrosscap_second line 21
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel_secondDerivative_comp line 47