subset_interior_iff_mem_nhdsSet

Mathlib.Topology.NhdsSet

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

English

s ⊆ interior t iff t ∈ nhdsSet s.

Русский

s ⊆ interior(t) тогда и только тогда, когда t ∈ nhdsSet s.

LaTeX

$$$s \\subseteq interior t \\iff t \\in nhdsSet s$$$

Lean4

theorem subset_interior_iff_mem_nhdsSet : s ⊆ interior t ↔ t ∈ 𝓝ˢ s := by
  simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]

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

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

Разделы

Аффилиация

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