OAI/Geometry/SplitTangent/SmoothLeafManifold.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth Leaf Manifold.

  1. def OAI.SplitTangent.LeafJetAtlas.smoothLeafOpen line 20
  2. lemma OAI.SplitTangent.LeafJetAtlas.smoothLeafOpen_nonempty line 24
  3. def OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.selectedChart line 30
  4. lemma OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.selectedChart_mem line 34
  5. def OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.chart line 38
  6. lemma OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.chart_mem line 43
  7. lemma OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.chart_source line 49
  8. lemma OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.chart_inverse_val line 53
  9. lemma OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.transition_holomorphic line 58
  10. def OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.chartedSpace line 79
  11. lemma OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.isManifold line 86
  12. def OAI.SplitTangent.LeafJetAtlas.SmoothLeafManifold.manifold line 98