image_mem_nhdsWithin — Mathlib

English

If f is inducing, then for x, s with s ∈ 𝓝 x, f '' s ∈ 𝓝[range f] f x.

Русский

Если f индуцирующее, то для любого x и s ∈ 𝓝 x верно f '' s ∈ 𝓝[range f] f x.

LaTeX

$$$\operatorname{IsInducing}(f) \Rightarrow \forall x, s, s \in \mathcal{N}(x) \Rightarrow f''s \in \mathcal{N}_{\mathrm{range}(f)}(f(x)).$$$

Lean4

theorem image_mem_nhdsWithin (hf : IsInducing f) {x : X} {s : Set X} (hs : s ∈ 𝓝 x) : f '' s ∈ 𝓝[range f] f x :=
  hf.map_nhds_eq x ▸ image_mem_map hs

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