α : Type u_1
β : Type ?u.17802
γ : Type ?u.17805
δ : Type ?u.17808
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
α : Type u_1
β : Type ?u.17802
γ : Type ?u.17805
δ : Type ?u.17808
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t
delta nhdsWithin
no goals
α : Type u_1
β : Type ?u.17802
γ : Type ?u.17805
δ : Type ?u.17808
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
rw [← inf_principal, inf_assoc]