no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.31315
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
x : α
y : β
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff, singleton_inter_nonempty, mem_preimage]