image_mem_nhds — Mathlib

English

If f approximates linear on s with a nonlinear right inverse and x has a neighborhood s in the domain, then the image f(s) contains a neighborhood of f(x).

Русский

Если f аппроксимируется линейно на s с нелинейным правым инверсом и вокруг x имеется окрестность s в области определения, то образ f(s) содержит окрестность точки f(x).

LaTeX

$$$hf: ApproximatesLinearOn(f,f',s,c) \land f'symm: f'.NonlinearRightInverse \land s \in 𝓝(x) \Rightarrow f''s \in 𝓝(f(x)).$$$

Lean4

theorem image_mem_nhds (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E} (hs : s ∈ 𝓝 x)
    (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) : f '' s ∈ 𝓝 (f x) :=
  by
  obtain ⟨t, hts, ht, xt⟩ : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := _root_.mem_nhds_iff.1 hs
  have := IsOpen.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt)
  exact mem_of_superset this (image_mono hts)

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