approximates_deriv_on_open_nhds — Mathlib

English

A comprehensive OpenPartialHomeomorph construction exists for HasStrictFDerivAt with invertible derivative and appropriate constants.

Русский

Существуют общие конструирования OpenPartialHomeomorph для HasStrictFDerivAt с обратимой производной и подходящими константами.

LaTeX

$$$\text{HasStrictFDerivAt } f f' a \Rightarrow \text{OpenPartialHomeomorph } E F$ (со всеми условиями)$$

Lean4

theorem approximates_deriv_on_open_nhds (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∃ s : Set E, a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (f' : E →L[𝕜] F) s (‖(f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2) :=
  by
  simp only [← and_assoc]
  refine ((nhds_basis_opens a).exists_iff fun s t => ApproximatesLinearOn.mono_set).1 ?_
  exact hf.approximates_deriv_on_nhds <| f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf'

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