∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (ϕ : τ → α → β) (s : Set α) {m : τ → τ}
  {f₁ f₂ : Filter τ}, Filter.Tendsto m f₁ f₂ → omegaLimit f₁ (fun t x => ϕ (m t) x) s ⊆ omegaLimit f₂ ϕ s