map_nhds_eq — Mathlib

English

If HasStrictDerivAt f f' a with f' ≠ 0, then mapping nhds preserves limit: map f (nhds a) = nhds (f a).

Русский

Если HasStrictDerivAt f f' a с f' ≠ 0, отображение nhds сохраняет предел: map f (nhds a) = nhds (f a).

LaTeX

$$$\text{HasStrictDerivAt } f f' a \wedge f' \neq 0 \Rightarrow \text{map } f (\mathcal{N}hds a) = \mathcal{N}hds (f a)$$$

Lean4

theorem map_nhds_eq : map f (𝓝 a) = 𝓝 (f a) :=
  (hf.hasStrictFDerivAt_equiv hf').map_nhds_eq_of_equiv

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