α : Type u_1
β : Type ?u.13810
γ : Type ?u.13813
δ : Type ?u.13816
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
α : Type u_1
β : Type ?u.13810
γ : Type ?u.13813
δ : Type ?u.13816
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a
delta nhdsWithin
no goals
α : Type u_1
β : Type ?u.13810
γ : Type ?u.13813
δ : Type ?u.13816
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
rw [← inf_sup_left, sup_principal]