OAI/Geometry/Immersion/ClosedSurface/TensorCoordinates.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ClosedSurfaceR4.RealModes.base_decompositionline 13 - lemma
OAI.ClosedSurfaceR4.RealModes.derivative_base_decompositionline 16 - lemma
OAI.ClosedSurfaceR4.RealModes.evaluate_realMetricTensorline 22 - lemma
OAI.ClosedSurfaceR4.RealModes.evaluate_realLinearizedTensorline 32 - lemma
OAI.ClosedSurfaceR4.RealModes.realMetricTensor_compline 45 - lemma
OAI.ClosedSurfaceR4.RealModes.realLinearizedTensor_compline 56 - lemma
OAI.ClosedSurfaceR4.RealModes.realOsc_compline 70 - lemma
OAI.ClosedSurfaceR4.RealModes.realLinearized_residual_compline 79