nhdsSet_le_sup'

Mathlib.Topology.NhdsSet

URI: https://scilib.ai/kg/mathlib#IsClosed.nhdsSet_le_sup'

English

Variant: 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 (tᶜ) when t is closed.

Русский

Вариант: 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 (tᶜ) при t замкнуто.

LaTeX

$$$ 𝓝ˢ s \le 𝓝ˢ (t \cap s) \sqcup 𝓟 (t^c) $$$

Lean4

theorem nhdsSet_le_sup' (h : IsClosed t) : 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 (tᶜ) := by rw [Set.inter_comm];
  exact h.nhdsSet_le_sup s

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

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

Разделы

Аффилиация

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