α : Type u_1
β : Type ?u.5955
γ : Type ?u.5958
δ : Type ?u.5961
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 (t'ᶜ)
α : Type u_1
β : Type ?u.5955
γ : Type ?u.5958
δ : Type ?u.5961
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x
rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]
no goals
α : Type u_1
β : Type ?u.5955
γ : Type ?u.5958
δ : Type ?u.5961
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 (t'ᶜ)
exact inter_mem_inf hs (mem_principal_self _)