OAI/Geometry/SplitTangent/AllCompactLeaves.lean
4 declarations, 0 contain sorry, 0 declared as axioms
All Compact Leaves.
- lemma
OAI.SplitTangent.LeafJetAtlas.all_closure_locallySinglePlaqueline 21 - theorem
OAI.SplitTangent.LeafJetAtlas.all_leaf_isClosedline 98 - theorem
OAI.SplitTangent.LeafJetAtlas.all_leaf_isCompactline 103 - theorem
OAI.SplitTangent.LeafJetAtlas.all_leaf_locallySinglePlaqueline 106