isOpenMap_of_hasStrictFDerivAt_equiv

English

If a function has invertible strict derivatives at every point (via a family of continuous linear equivalences), then it is an open map.

Русский

Если на всей области функция имеет обобщённую обратимую строгую производную через семейство линейных эквивалентностей, то она является открытым отображением.

LaTeX

$$$ \text{IsOpenMap}(f) \quad \text{given } \forall x,\ HasStrictFDerivAt f (f'(x)) x $$$

Lean4

/-- If a function has an invertible strict derivative at all points, then it is an open map. -/
theorem isOpenMap_of_hasStrictFDerivAt_equiv [CompleteSpace E] {f : E → F} {f' : E → E ≃L[𝕜] F}
    (hf : ∀ x, HasStrictFDerivAt f (f' x : E →L[𝕜] F) x) : IsOpenMap f :=
  isOpenMap_iff_nhds_le.2 fun x => (hf x).map_nhds_eq_of_equiv.ge

Похожие утверждения