OAI/Geometry/SplitTangent/DenseCompactLeaves.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dense Compact Leaves.

  1. def OAI.SplitTangent.TangentSplitting.positiveLocus line 21
  2. lemma OAI.SplitTangent.TangentSplitting.submersive_range_positive line 25
  3. lemma OAI.SplitTangent.TangentSplitting.dense_interior_positiveLocus line 34
  4. theorem OAI.SplitTangent.TangentSplitting.exists_dense_open_compact_leaves line 51