OAI/Geometry/SplitTangent/OpenManifold.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Open Manifold.

  1. abbrev OAI.SplitTangent.OpenManifold.Carrier line 16
  2. theorem OAI.SplitTangent.OpenManifold.nonempty line 18
  3. def OAI.SplitTangent.OpenManifold.val line 19
  4. lemma OAI.SplitTangent.OpenManifold.isOpenEmbedding_val line 21
  5. def OAI.SplitTangent.OpenManifold.manifold line 24
  6. lemma OAI.SplitTangent.OpenManifold.val_holomorphic line 35
  7. lemma OAI.SplitTangent.OpenManifold.val_mem line 40
  8. lemma OAI.SplitTangent.OpenManifold.range_val line 42
  9. lemma OAI.SplitTangent.OpenManifold.val_mfderiv_bijective line 46