isInvariant_omegaLimit — Mathlib

English

If the translation maps t ↦ t + · are all continuous in the filter sense, then the ω-limit set is invariant under the Flow.

Русский

Если переходы по времени сохраняют структуру, ω‑лимит invariantsi и под действием потока.

LaTeX

$$$ (\forall t, Tendsto (t + ·) f f) \Rightarrow IsInvariant ϕ (\omega f ϕ s). $$$

Lean4

theorem isInvariant_omegaLimit (hf : ∀ t, Tendsto (t + ·) f f) : IsInvariant ϕ (ω f ϕ s) :=
  by
  refine fun t ↦ MapsTo.mono_right ?_ (omegaLimit_subset_of_tendsto ϕ s (hf t))
  exact mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm) (continuous_const.flow ϕ continuous_id)

Похожие утверждения