OAI/Geometry/SplitTangent/FoliationLeaves.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Foliation Leaves.

  1. structure OAI.PlaqueSystem line 11
  2. def OAI.PlaqueSystem.Related line 21
  3. def OAI.PlaqueSystem.Reachable line 25
  4. def OAI.PlaqueSystem.leaf line 27
  5. lemma OAI.PlaqueSystem.Related.symm line 29
  6. lemma OAI.PlaqueSystem.Reachable.refl line 33
  7. lemma OAI.PlaqueSystem.Reachable.trans line 34
  8. lemma OAI.PlaqueSystem.Reachable.symm line 36
  9. lemma OAI.PlaqueSystem.leaf_saturated line 41
  10. lemma OAI.PlaqueSystem.related_in_rectangle line 44
  11. theorem OAI.PlaqueSystem.closure_saturated line 52
  12. def OAI.PlaqueSystem.LocallySinglePlaque line 86
  13. theorem OAI.PlaqueSystem.leaf_isClosed_of_locallySinglePlaque line 92
  14. theorem OAI.PlaqueSystem.locallySinglePlaque_of_finite_transversal line 113