union_mem_nhdsSet — Mathlib

English

If s1 ∈ 𝓝ˢ t1 and s2 ∈ 𝓝ˢ t2, then s1 ∪ s2 ∈ 𝓝ˢ (t1 ∪ t2).

Русский

Если s1 ∈ 𝓝ˢ t1 и s2 ∈ 𝓝ˢ t2, то s1 ∪ s2 ∈ 𝓝ˢ (t1 ∪ t2).

LaTeX

$$$ (s_1 \in 𝓝ˢ t_1) \rightarrow (s_2 \in 𝓝ˢ t_2) \rightarrow s_1 \cup s_2 \in 𝓝ˢ (t_1 \cup t_2) $$$

Lean4

theorem union_mem_nhdsSet (h₁ : s₁ ∈ 𝓝ˢ t₁) (h₂ : s₂ ∈ 𝓝ˢ t₂) : s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂) :=
  by
  rw [nhdsSet_union]
  exact union_mem_sup h₁ h₂

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