image_mem_nhdsWithin — Mathlib

English

If s is a neighborhood of x, then its image under I lies in the nhdsWithin neighborhood of I(x) inside range I.

Русский

Если s — окрестность точки x, то образ s под I лежит в nhdsWithin окрестности точки I(x) внутри range(I).

LaTeX

$$If s \\in 𝓝 x, then I''s ∈ 𝓝[range I] I x$$

Lean4

theorem image_mem_nhdsWithin {x : H} {s : Set H} (hs : s ∈ 𝓝 x) : I '' s ∈ 𝓝[range I] I x :=
  I.map_nhds_eq x ▸ image_mem_map hs

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