OAI/Geometry/PrescribedRicci/PathUniformAtlas.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Path Uniform Atlas.

  1. structure OAI.Anticanonical.SourceSmooth.UniformPathPatch line 23
  2. def OAI.Anticanonical.SourceSmooth.UniformPathPatch.source line 45
  3. lemma OAI.Anticanonical.SourceSmooth.UniformPathPatch.isOpen_source line 48
  4. lemma OAI.Anticanonical.SourceSmooth.UniformPathPatch.source_sub line 51
  5. lemma OAI.Anticanonical.SourceSmooth.UniformPathPatch.center_target line 54
  6. theorem OAI.Anticanonical.SourceSmooth.UniformPathPatch.exists_at line 57
  7. theorem OAI.Anticanonical.SourceSmooth.UniformPathPatch.finite_cover line 96
  8. theorem OAI.Anticanonical.SourceSmooth.exists_uniform_path_localizers line 108