nhdsSet_union — Mathlib

English

The set-neighborhoods of a union equal the supremum of the set-neighborhoods: 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t.

Русский

Окрестности множества объединения равны верхней границе окрестностей: 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t.

LaTeX

$$$ 𝓝ˢ (s \cup t) = 𝓝ˢ s \bigsqcup 𝓝ˢ t $$$

Lean4

@[simp]
theorem nhdsSet_union (s t : Set X) : 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t := by simp only [nhdsSet, image_union, sSup_union]

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