OAI/Geometry/SplitTangent/CompactPositiveLeaf.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact Positive Leaf.

  1. lemma OAI.SplitTangent.RationalCurveFrames.closure_locallySinglePlaque line 28
  2. theorem OAI.SplitTangent.RationalCurveFrames.leaf_isClosed line 109
  3. theorem OAI.SplitTangent.RationalCurveFrames.leaf_isCompact line 114
  4. theorem OAI.SplitTangent.TangentSplitting.exists_compact_leaf line 126