image_mem_nhds — Mathlib

English

For an open embedding f, f''s ∈ nhds (f x) iff s ∈ nhds x.

Русский

Для открытого вложения f имеет место: f''s ∈ nhds(f x) эквивалентно s ∈ nhds x.

LaTeX

$$$ f \text{ isOpenEmbedding } \Rightarrow ( f''s \in \mathcal{N}(f x) \iff s \in \mathcal{N}(x) ) $$$

Lean4

theorem image_mem_nhds {f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {x : X} : f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x := by
  rw [← hf.map_nhds_eq, mem_map, preimage_image_eq _ hf.injective]

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