OAI/Geometry/IsometricImmersion/Obstructions/PatchObstructionSet.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Perturbation.patchObstructionSet line 13
2. theorem OAI.SmoothLocal.Perturbation.patchObstructionSet_isGdelta line 16
3. theorem OAI.SmoothLocal.Perturbation.mem_patchObstructionSet_iff line 20
4. theorem OAI.SmoothLocal.Perturbation.patchObstructionSet_has_no_admissible_height line 26
5. theorem OAI.SmoothLocal.Perturbation.patchObstructionSet_subset_complement_admissible line 35