OAI/Geometry/SplitTangent/RationalVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rational Variation.

  1. theorem OAI.SplitTangent.RationallyConnected.exists_submersive_familyAlternative line 21
  2. theorem OAI.SplitTangent.TangentSplitting.integrable_of_rationallyConnected line 93
  3. theorem OAI.SplitTangent.RationallyConnected.exists_submersive_family line 108
  4. def OAI.SplitTangent.IntegrabilityStatement line 183

    Also declared: ComparatorChallenges/SplitTangentIntegrability.lean:130 (same declaration text).

  5. theorem OAI.SplitTangent.integrability_main line 188

    Distinct definitions of this name: ComparatorChallenges/SplitTangentIntegrability.lean:135 (same statement text; different proof or body). Qualify references as OAI.SplitTangent.integrability_main@path.