nhds_le_nhdsSet

Mathlib.Topology.NhdsSet

URI: https://scilib.ai/kg/mathlib#nhds_le_nhdsSet

English

If x ∈ s, then the neighborhood filter at x is ≤ 𝓝ˢ s.

Русский

Если x ∈ s, то фильтр окрестностей в точке x меньше или равен 𝓝ˢ s.

LaTeX

$$$ (x \in s) \Rightarrow 𝓝 x \le 𝓝ˢ s $$$

Lean4

theorem nhds_le_nhdsSet (h : x ∈ s) : 𝓝 x ≤ 𝓝ˢ s :=
  le_sSup <| mem_image_of_mem _ h

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

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

Разделы

Аффилиация

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