mem_nhdsSet_iff_forall

Mathlib.Topology.NhdsSet

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

English

s ∈ 𝓝ˢ t iff ∀ x, x ∈ t → s ∈ 𝓝 x.

Русский

s принадлежит 𝓝ˢ t тогда и только тогда, когда для всех x ∈ t выполняется s ∈ 𝓝 x.

LaTeX

$$$s \\in nhdsSet t \\iff \\forall x, x \\in t \\to s \\in nhds x$$$

Lean4

theorem mem_nhdsSet_iff_forall : s ∈ 𝓝ˢ t ↔ ∀ x : X, x ∈ t → s ∈ 𝓝 x := by
  simp_rw [nhdsSet, Filter.mem_sSup, forall_mem_image]

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

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

Разделы

Аффилиация

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