isOpenMap_of_hasStrictDerivAt — Mathlib

English

If HasStrictDerivAt f f' x with f'(x) ≠ 0 for all x, then f is an open map.

Русский

Если у функции f в каждой точке производная не нулевая, то f является открытым отображением.

LaTeX

$$$\forall x, \ HasStrictDerivAt f (f'(x)) x \land \forall x, f'(x) \neq 0 \Rightarrow \text{IsOpenMap } f$$$

Lean4

/-- If a function has a non-zero strict derivative at all points, then it is an open map. -/
theorem isOpenMap_of_hasStrictDerivAt {f' : 𝕜 → 𝕜} (hf : ∀ x, HasStrictDerivAt f (f' x) x) (h0 : ∀ x, f' x ≠ 0) :
    IsOpenMap f :=
  isOpenMap_iff_nhds_le.2 fun x => ((hf x).map_nhds_eq (h0 x)).ge

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