open_map_of_strict_deriv

theorem open_map_of_strict_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {f f' : 𝕜 → 𝕜}, (∀ (x : 𝕜), HasStrictDerivAt f (f' x) x) → (∀ (x : 𝕜), f' x ≠ 0) → IsOpenMap f

The theorem `open_map_of_strict_deriv` states that if a function `f` has a non-zero strict derivative at all points in a nontrivially normed field `𝕜` that is also a complete space, then `f` is an open map. This means that for every point `x` in `𝕜`, the function has a derivative `f'` such that `f'` at `x` is not zero, and for any open set `U` in `𝕜`, the image of `U` under `f` is also an open set.

More concisely: If a function `f` with non-zero strict derivative at all points in the complete, nontrivially normed field `𝕜` is a open map, then for every open set `U` in `𝕜`, the image `f(U)` is also an open set.