LocalSubmersion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local open mapping consequence needed for Cartan multiplication

This is a direct chartwise application of Mathlib's strict inverse function theorem. It uses a surjective differential, without requiring complementary Cartan factors or assuming a local product theorem.

theorem OAI.PolycyclicRecognition.map_nhds_eq_of_surjective_mfderiv line 34
Source documentation
A continuously differentiable map with surjective differential sends the neighborhood filter exactly onto the neighborhood filter of its value.
```
theorem map_nhds_eq_of_surjective_mfderiv
    (hf : ContMDiffAt I J 1 f x)
    (hsurj : Function.Surjective (mfderiv I J f x)) :
    map f (𝓝 x) = 𝓝 (f x) := by
…
```