OAI/Geometry/SplitTangent/EmbeddedLeafCharts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Embedded Leaf Charts.

  1. structure OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart line 31
  2. lemma OAI.SplitTangent.LeafJetAtlas.exists_embeddedLeafChart line 38
  3. def OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.rankEquiv line 65
  4. def OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.chart line 72
  5. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.mem_source line 75
  6. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.source_ambient line 79
  7. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.target_pair line 84
  8. def OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.forward line 91
  9. def OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.inverse line 92
  10. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.forward_eq line 95
  11. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.inverse_eq line 99
  12. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.forward_holomorphic line 106
  13. lemma OAI.SplitTangent.LeafJetAtlas.EmbeddedLeafChart.inverse_holomorphic line 112
  14. def OAI.SplitTangent.LeafJetAtlas.embeddedAtlas line 122