OAI/Geometry/SplitTangent/RCCovariantVanishing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

R C Covariant Vanishing.

  1. structure OAI.SplitTangent.HolomorphicTangentTensor line 21
  2. def OAI.SplitTangent.HolomorphicTangentTensor.coordinates line 31
  3. lemma OAI.SplitTangent.HolomorphicTangentTensor.coordinates_zero_iff line 35
  4. def OAI.SplitTangent.HolomorphicTangentTensor.along line 57
  5. lemma OAI.SplitTangent.HolomorphicTangentTensor.zero_on_positive_curve line 72
  6. lemma OAI.SplitTangent.HolomorphicTangentTensor.local_analytic_zero_locus line 78
  7. lemma OAI.SplitTangent.HolomorphicTangentTensor.eq_zero_of_nonempty_open line 103
  8. theorem OAI.SplitTangent.RationallyConnected.exists_open_positive_tangent_curves line 125
  9. theorem OAI.SplitTangent.RationallyConnected.holomorphic_tensor_zero line 140
  10. theorem OAI.SplitTangent.RationallyConnected.holomorphic_cover_tensor_zero line 152