OAI/Geometry/SplitTangent/LeafProducts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Leaf Products.

  1. lemma OAI.SplitTangent.TangentSplitting.ext_projector line 20
  2. lemma OAI.SplitTangent.TangentSplitting.swap_swap_eq line 27
  3. lemma OAI.SplitTangent.LeafJetAtlas.leaf_cast line 37
  4. theorem OAI.SplitTangent.LeafJetAtlas.compatible_projective_product_of_leafPair_injective line 50