α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
x : α
F : Filter ι
u : ι → α
⊢ (∀ {p : α → Prop}, (∀ᶠ (x : α) in 𝓝 x, p x) → ∃ᶠ (a : ι) in F, p (u a)) ↔
    ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (a : ι) in F, u a ∈ s
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
x : α
F : Filter ι
u : ι → α
⊢ MapClusterPt x F u ↔ ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (a : ι) in F, u a ∈ s
simp_rw [MapClusterPt, ClusterPt, inf_neBot_iff_frequently_left, frequently_map]
no goals
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
x : α
F : Filter ι
u : ι → α
⊢ (∀ {p : α → Prop}, (∀ᶠ (x : α) in 𝓝 x, p x) → ∃ᶠ (a : ι) in F, p (u a)) ↔
    ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (a : ι) in F, u a ∈ s
rfl