OAI/Geometry/NodalSets/Charts/SupportedFiniteAtlasBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.sphereAtlasCore line 14
  2. lemma OAI.Yau.Target.sphereAtlasCore_compact line 16
  3. theorem OAI.Yau.Target.finite_sphere_coefficient_atlas line 19
  4. def OAI.Yau.Target.sphereCoefficientDistance line 31
  5. theorem OAI.Yau.Target.supported_finite_atlas_coefficient_bound line 36