OAI/Geometry/IsometricImmersion/Obstructions/PatchResidualTheorem.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Perturbation.patchObstructionSet_dense line 14
2. theorem OAI.SmoothLocal.Perturbation.no_admissible_height_residual line 27
3. theorem OAI.SmoothLocal.Perturbation.exists_patch_obstruction_in_open line 42
4. theorem OAI.SmoothLocal.Perturbation.exists_patch_obstruction_in_neighborhood line 57