subset_of_mem_nhdsSet

Mathlib.Topology.NhdsSet

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

English

If t is a member of the set-neighborhoods filter of s, then s is contained in t.

Русский

Если t является элементом фильтра множеств-окрестностей s, значит s ⊆ t.

LaTeX

$$$ t \in 𝓝ˢ s \Rightarrow s \subseteq t $$$

Lean4

theorem subset_of_mem_nhdsSet (h : t ∈ 𝓝ˢ s) : s ⊆ t :=
  principal_le_nhdsSet h

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

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

Разделы

Аффилиация

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