OAI/Geometry/SurfaceImmersion/Whitney/SurfacePairPointAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual chart translations can avoid prescribed finite surface points while retaining transversality at all remaining coincidences.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surface_pair_patch_translation_avoiding_points line 16