nhdsSet_sInter_le

Mathlib.Topology.NhdsSet

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

English

For a set s of sets, 𝓝ˢ (⋂₀ s) ≤ ⨅ x ∈ s, 𝓝ˢ x.

Русский

Для множества множест s: 𝓝ˢ (⋂₀ s) ≤ ⨅ x ∈ s, 𝓝ˢ x.

LaTeX

$$$ 𝓝ˢ (\bigcap_0 s) \le \bigsqcap_{x \in s} 𝓝ˢ x $$$

Lean4

theorem nhdsSet_sInter_le (s : Set (Set X)) : 𝓝ˢ (⋂₀ s) ≤ ⨅ x ∈ s, 𝓝ˢ x :=
  (monotone_nhdsSet (X := X)).map_sInf_le

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

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

Разделы

Аффилиация

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