OAI/Geometry/SplitTangent/ProjectiveTangentBox.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Projective Tangent Box.

  1. instance OAI.SplitTangent.FormalCauchy.projectiveTangentBoxAnalyticFunctionCoeFun line 24
  2. theorem OAI.SplitTangent.TangentSplitting.coordinateCurve_analyticAlternative line 38
  3. def OAI.SplitTangent.TangentSplitting.localJetAlternative line 48