mem_nhdsSet_iff_exists

Mathlib.Topology.NhdsSet

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

English

s ∈ nhdsSet t iff ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s.

Русский

s принадлежит nhdsSet t тогда, когда существует открытое U с t ⊆ U ⊆ s.

LaTeX

$$$s \\in nhdsSet t \\iff \\exists U, IsOpen U \\land t \\subseteq U \\land U \\subseteq s$$$

Lean4

theorem mem_nhdsSet_iff_exists : s ∈ 𝓝ˢ t ↔ ∃ U : Set X, IsOpen U ∧ t ⊆ U ∧ U ⊆ s := by
  rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]

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

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

Разделы

Аффилиация

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