α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : α → Prop
a : α
⊢ (¬∃ᶠ (y : α) in 𝓝 a, ∃ᶠ (x : α) in 𝓝 y, p x) ↔ ¬∃ᶠ (x : α) in 𝓝 a, p x
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : α → Prop
a : α
⊢ (∃ᶠ (y : α) in 𝓝 a, ∃ᶠ (x : α) in 𝓝 y, p x) ↔ ∃ᶠ (x : α) in 𝓝 a, p x
rw [← not_iff_not]
no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : α → Prop
a : α
⊢ (¬∃ᶠ (y : α) in 𝓝 a, ∃ᶠ (x : α) in 𝓝 y, p x) ↔ ¬∃ᶠ (x : α) in 𝓝 a, p x
simp only [not_frequently, eventually_eventually_nhds]