OAI/Geometry/PrescribedPotential/AtlasLocalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Atlas Localization.

  1. def OAI.Anticanonical.ComplexAtlas.chartedSpace line 20
  2. lemma OAI.Anticanonical.ComplexAtlas.real_smooth_transition line 26
  3. theorem OAI.Anticanonical.ComplexAtlas.isManifold line 33
  4. theorem OAI.Anticanonical.ComplexAtlas.contMDiff_iff line 45
  5. theorem OAI.Anticanonical.ComplexAtlas.exists_smooth_partition line 67