map_nhds_eq — Mathlib

English

Under the same hypotheses, the pushforward of the neighborhood filter by f equals the neighborhood filter at f(x): map f (𝓝 x) = 𝓝 (f x).

Русский

При тех же гипотезах перенос фильтра окрестностей по f совпадает с окрестностями в f(x): map f (𝓝 x) = 𝓝 (f x).

LaTeX

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

Lean4

theorem map_nhds_eq (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E} (hs : s ∈ 𝓝 x)
    (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) : map f (𝓝 x) = 𝓝 (f x) :=
  by
  refine le_antisymm ((hf.continuousOn x (mem_of_mem_nhds hs)).continuousAt hs) (le_map fun t ht => ?_)
  have : f '' (s ∩ t) ∈ 𝓝 (f x) := (hf.mono_set inter_subset_left).image_mem_nhds f'symm (inter_mem hs ht) hc
  exact mem_of_superset this (image_mono inter_subset_right)

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