FiniteCrosscapCancellation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reprepare the double points between genuine cancellations. The singular set strictly decreases, while all remaining quadratic germs are retained.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.cancel_finite_quadratic_pair line 16
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.remove_finite_quadratic_crosscaps line 55
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_three_space_immersion line 90
Source documentation
Whitney's compact surface immersion, with smoothness retained.
```
theorem smooth_three_space_immersion :
    ∃ f : M → ProjectionTarget 3, ContMDiff planeModel 𝓘(ℝ,ProjectionTarget 3) ∞ f ∧
      ∀ x, Function.Injective (mfderiv planeModel 𝓘(ℝ,ProjectionTarget 3) f x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ProjectionTarget, OAI.ClosedSurfaceR4.planeModel