map_nhds_eq_of_surj — Mathlib

English

There exists an open nhds neighborhood on which ApproximatesLinearOn holds with a positive bound.

Русский

Существует открытое множество вокруг a, на котором выполняется ApproximatesLinearOn со стойким положительным значением константы.

LaTeX

$$$\exists s \in 𝓝 a,\ IsOpen s \land ApproximatesLinearOn f f' s (‖(f'.symm)‖^{-1}/2)$$$

Lean4

theorem map_nhds_eq_of_surj [CompleteSpace E] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
    (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) (h : LinearMap.range f' = ⊤) : map f (𝓝 a) = 𝓝 (f a) :=
  by
  let f'symm := f'.nonlinearRightInverseOfSurjective h
  set c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2 with hc
  have f'symm_pos : 0 < f'symm.nnnorm := f'.nonlinearRightInverseOfSurjective_nnnorm_pos h
  have cpos : 0 < c := by simp [hc, inv_pos, f'symm_pos]
  obtain ⟨s, s_nhds, hs⟩ : ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c := hf.approximates_deriv_on_nhds (Or.inr cpos)
  apply hs.map_nhds_eq f'symm s_nhds (Or.inr (NNReal.half_lt_self _))
  simp [ne_of_gt f'symm_pos]

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