OAI/Geometry/IsometricImmersion/Caps/BoundedClassReflection.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SmoothLocal.Geometry.PatchAdmissibleHeight.reflectedline 14 - theorem
OAI.SmoothLocal.Geometry.BoundedAdmissibleHeight.reflectedline 37 - theorem
OAI.SmoothLocal.Geometry.bounded_class_reflected_centerline 53 - theorem
OAI.SmoothLocal.Perturbation.reflected_actual_metric_zero_patchline 71