α : Type u_1
β : Type ?u.11749
γ : Type ?u.11752
δ : Type ?u.11755
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a
α : Type u_1
β : Type ?u.11749
γ : Type ?u.11752
δ : Type ?u.11755
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝 a
rw [← nhdsWithin_univ]
case h
α : Type u_1
β : Type ?u.11749
γ : Type ?u.11752
δ : Type ?u.11755
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a
α : Type u_1
β : Type ?u.11749
γ : Type ?u.11752
δ : Type ?u.11755
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a
apply nhdsWithin_le_of_mem
no goals
case h
α : Type u_1
β : Type ?u.11749
γ : Type ?u.11752
δ : Type ?u.11755
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a
exact univ_mem