image_mem_nhds

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.image_mem_nhds

English

If s is a neighborhood of x, then e''s is a neighborhood of e(x).

Русский

Если s — окрестность x, то образ e''s — окрестность e(x).

LaTeX

$$$\\forall x,\\; s \\in \\mathcal{N}(x) \\Rightarrow e'' s \\in \\mathcal{N}(e(x))$$$

Lean4

theorem image_mem_nhds {x} (hx : x ∈ e.source) {s : Set X} (hs : s ∈ 𝓝 x) : e '' s ∈ 𝓝 (e x) :=
  e.map_nhds_eq hx ▸ Filter.image_mem_map hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru