OAI/Geometry/IsometricImmersion/Metrics/PatchTensorPositivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Geometry.patchAddress_inverse_mulVec_injective line 12
2. theorem OAI.SmoothLocal.Geometry.patchAddress_local_inverse_congruence line 20
3. theorem OAI.SmoothLocal.Geometry.patchAddress_add_posDef_of_local_metric line 34
4. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_smoothPositive_of_local_metrics line 53
5. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_curvature_on_disk_of_local_metrics line 62