α : Type u_1
β : Type ?u.3293
γ : Type ?u.3296
δ : Type ?u.3299
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x
α : Type u_1
β : Type ?u.3293
γ : Type ?u.3296
δ : Type ?u.3299
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
refine' ⟨fun h => _, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
α : Type u_1
β : Type ?u.3293
γ : Type ?u.3296
δ : Type ?u.3299
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
α : Type u_1
β : Type ?u.3293
γ : Type ?u.3296
δ : Type ?u.3299
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x
simp only [eventually_nhdsWithin_iff] at h⊢
no goals
α : Type u_1
β : Type ?u.3293
γ : Type ?u.3296
δ : Type ?u.3299
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs