mem_of_mem_nhds

Mathlib.Topology.Neighborhoods

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

English

If a set s is in the neighborhood filter at x, then x ∈ s.

Русский

Если s принадлежит фильтру окрестностей x, то x ∈ s.

LaTeX

$$$\\text{mem\_of\_mem\_nhds}:\\; s \\in \\mathcal N(x) \\Rightarrow x \\in s$$$

Lean4

theorem mem_of_mem_nhds : s ∈ 𝓝 x → x ∈ s := fun H =>
  let ⟨_t, ht, _, hs⟩ := mem_nhds_iff.1 H;
  ht hs

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

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

Разделы

Аффилиация

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