α : Type u_1
β : Type ?u.18144
γ : Type ?u.18147
δ : Type ?u.18150
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a
α : Type u_1
β : Type ?u.18144
γ : Type ?u.18147
δ : Type ?u.18150
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s ∩ t] a = 𝓝[t] a
rw [nhdsWithin_inter, inf_eq_right]
no goals
α : Type u_1
β : Type ?u.18144
γ : Type ?u.18147
δ : Type ?u.18150
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a
exact nhdsWithin_le_of_mem h