closedBall_subset_target — Mathlib

English

A closed ball around f(b) is contained in the target set of the approximated inverse.

Русский

Замкнутый шар вокруг f(b) содержится в целевом множестве аппроксимируемого обратного отображения.

LaTeX

$$$\mathrm{closedBall}(f(b), (N^{-1} - c) \cdot \varepsilon) \subseteq (hf.toOpenPartialHomeomorph f s hc hs).target$$$

Lean4

theorem closedBall_subset_target (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹)
    (hs : IsOpen s) {b : E} (ε0 : 0 ≤ ε) (hε : closedBall b ε ⊆ s) :
    closedBall (f b) ((N⁻¹ - c) * ε) ⊆ (hf.toOpenPartialHomeomorph f s hc hs).target :=
  (hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse ε0 hε).mono hε Subset.rfl

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