OAI/Geometry/SplitTangent/TwistedCurveTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Twisted Curve Tensor.

  1. abbrev OAI.SplitTangent.TangentTensor line 18
  2. def OAI.SplitTangent.tangentTensorCoordinates line 22
  3. structure OAI.SplitTangent.TwistedCurveTensor line 30
  4. lemma OAI.SplitTangent.section_coordinates_analytic line 39
  5. lemma OAI.SplitTangent.tangentTensor_contract_analytic line 52
  6. def OAI.SplitTangent.TwistedCurveTensor.contract line 83
  7. theorem OAI.SplitTangent.TwistedCurveTensor.contract_zero line 100
  8. theorem OAI.SplitTangent.TwistedCurveTensor.vanish_on_generated_fiber line 130