OAI/Geometry/SplitTangent/CompactLeafQuotient.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Compact Leaf Quotient.

  1. lemma OAI.SplitTangent.LeafJetAtlas.isClosed_range_compactLeaf line 24
  2. lemma OAI.SplitTangent.LeafJetAtlas.compactLeaf_eq_of_mem line 30
  3. lemma OAI.SplitTangent.LeafJetAtlas.isClosed_graph_compactLeaf line 34
  4. lemma OAI.SplitTangent.LeafJetAtlas.continuous_compactLeaf line 54
  5. def OAI.SplitTangent.LeafJetAtlas.CompactLeafSpace line 71
  6. instance OAI.SplitTangent.LeafJetAtlas.compactSpace_compactLeafSpace line 73
  7. def OAI.SplitTangent.LeafJetAtlas.leafQuotient line 76
  8. lemma OAI.SplitTangent.LeafJetAtlas.continuous_leafQuotient line 79
  9. lemma OAI.SplitTangent.LeafJetAtlas.surjective_leafQuotient line 82
  10. lemma OAI.SplitTangent.LeafJetAtlas.leafQuotient_eq_iff line 86
  11. lemma OAI.SplitTangent.LeafJetAtlas.isQuotientMap_leafQuotient line 96
  12. lemma OAI.SplitTangent.LeafJetAtlas.isClosedMap_leafQuotient line 100
  13. lemma OAI.SplitTangent.LeafJetAtlas.leafQuotient_image line 103
  14. lemma OAI.SplitTangent.LeafJetAtlas.isOpenMap_leafQuotient line 120
  15. lemma OAI.SplitTangent.LeafJetAtlas.isOpenQuotientMap_leafQuotient line 125
  16. instance OAI.SplitTangent.LeafJetAtlas.connectedSpace_compactLeafSpace line 129