case intro.intro
α : Type u_1
β : Type ?u.6425
γ : Type ?u.6428
δ : Type ?u.6431
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a
α : Type u_1
β : Type ?u.6425
γ : Type ?u.6428
δ : Type ?u.6431
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
⊢ t ∈ 𝓝 a
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.6425
γ : Type ?u.6428
δ : Type ?u.6431
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a
exact (nhds a).sets_of_superset ((nhds a).inter_sets Hw h1) hw