OAI/Geometry/SplitTangent/IntegrabilityReduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integrability Reduction.

  1. lemma OAI.SplitTangent.LeafJetAtlas.leafPair_injective_of_compatible_projective_product line 25
  2. theorem OAI.SplitTangent.LeafJetAtlas.compatible_projective_product_iff_leafPair_injective line 68
  3. lemma OAI.SplitTangent.LeafJetAtlas.leafPair_injective_iff_single_intersection line 73
  4. def OAI.SplitTangent.LeafPairOneSheetedStatement line 89
  5. theorem OAI.SplitTangent.main_iff_leafPair_oneSheeted line 97