∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [CompactSpace β] {v : Set β}, IsOpen v → omegaLimit f ϕ s ⊆ v → ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s v