τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f (fun t_1 x => toFun ϕ (t_1 + t) x) s ⊆ ω f ϕ.toFun s
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f ϕ.toFun (toFun ϕ t '' s) ⊆ ω f ϕ.toFun s
simp only [omegaLimit_image_eq, ← map_add]
no goals
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f (fun t_1 x => toFun ϕ (t_1 + t) x) s ⊆ ω f ϕ.toFun s
exact omegaLimit_subset_of_tendsto ϕ s ht