omegaLimit_image_eq — Mathlib

English

Under suitable regularity, the omega-limit of the image equals the omega-limit of the original set.

Русский

При определённой регулярности ω‑лимит образа равен ω‑лимиту исходного множества.

LaTeX

$$$ \omega f ϕ (ϕ t '' s) = \omega f ϕ s \quad\text{(under suitable hypotheses)}. $$$

Lean4

/-- the ω-limit of a forward image of `s` is the same as the ω-limit of `s`. -/
@[simp]
theorem omegaLimit_image_eq (hf : ∀ t, Tendsto (· + t) f f) (t : τ) : ω f ϕ (ϕ t '' s) = ω f ϕ s :=
  Subset.antisymm (omegaLimit_image_subset _ _ _ _ (hf t)) <|
    calc
      ω f ϕ s = ω f ϕ (ϕ (-t) '' (ϕ t '' s)) := by simp [image_image, ← map_add]
      _ ⊆ ω f ϕ (ϕ t '' s) := omegaLimit_image_subset _ _ _ _ (hf _)

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