nhds_le

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#IsOpenMap.nhds_le

English

For an open map f and each x, nhds(f(x)) ≤ map f (nhds(x)).

Русский

Для открытого отображения f и каждого x выполняется nhds(f(x)) ≤ map f (nhds(x)).

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall x, \\ NHDS(f(x)) \\le map(f)(NHDS(x))$$$$

Lean4

theorem nhds_le (hf : IsOpenMap f) (x : X) : 𝓝 (f x) ≤ map f (𝓝 x) :=
  le_map fun _ => hf.image_mem_nhds

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

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

Разделы

Аффилиация

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