OAI/Geometry/NodalSets/Charts/SphereFiniteVariationalFrame.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Yau.Target.sphere_resolvent_finite_variational_frameline 14 - theorem
OAI.Yau.Target.sphere_resolvent_finite_smooth_frameline 29