τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
t : τ
⊢ MapsTo (toFun ϕ t) (ω f ϕ.toFun s) (ω f (fun t_1 x => toFun ϕ ((fun x x_1 => x + x_1) t t_1) x) s)
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)
refine' fun t ↦ MapsTo.mono_right _ (omegaLimit_subset_of_tendsto ϕ s (hf t))
no goals
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
t : τ
⊢ MapsTo (toFun ϕ t) (ω f ϕ.toFun s) (ω f (fun t_1 x => toFun ϕ ((fun x x_1 => x + x_1) t t_1) x) s)
exact
  mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm)
    (continuous_const.flow ϕ continuous_id)