omegaLimit_image_subset — Mathlib

English

If t advances by t, then the omega-limit of the image of s under ϕ t is contained in the omega-limit of s.

Русский

Если перейти по времени t, ω‑лимит образа s под действием ϕ t содержится в ω‑лимите s.

LaTeX

$$$ \omega f ϕ (ϕ t '' s) \subseteq \omega f ϕ s. $$$

Lean4

theorem omegaLimit_image_subset (t : τ) (ht : Tendsto (· + t) f f) : ω f ϕ (ϕ t '' s) ⊆ ω f ϕ s :=
  by
  simp only [omegaLimit_image_eq, ← map_add]
  exact omegaLimit_subset_of_tendsto ϕ s ht

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