OAI/Geometry/SplitTangent/GlobalTopologicalProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Global Topological Product.

  1. def OAI.SplitTangent.LeafJetAtlas.leafPair line 24
  2. lemma OAI.SplitTangent.LeafJetAtlas.continuous_leafPair line 28
  3. lemma OAI.SplitTangent.LeafJetAtlas.leafPair_rectangle_image line 31
  4. lemma OAI.SplitTangent.LeafJetAtlas.leafPair_rectangle_image_open line 58
  5. lemma OAI.SplitTangent.LeafJetAtlas.isOpenMap_leafPair line 70
  6. lemma OAI.SplitTangent.LeafJetAtlas.surjective_leafPair line 98
  7. lemma OAI.SplitTangent.LeafJetAtlas.leafPair_fiber_eq line 104
  8. lemma OAI.SplitTangent.LeafJetAtlas.leafPair_fiber_finite line 118