mem_omegaLimit_singleton_iff_map_cluster_point

English

A point y is in the ω-limit of the singleton {x} with respect to f and ϕ iff y is a MapClusterPt of y with respect to f and the map t ↦ ϕ t x.

Русский

Точка y принадлежит ω‑лимиту множества‑синглтона {x} по отношению к f и ϕ тогда, когда y является MapClusterPt для y по отношению к f и отображению t ↦ ϕ t x.

LaTeX

$$$ y \in \omega f ϕ \{ x \} \iff MapClusterPt y f (\lambda t. ϕ t x). $$$

Lean4

/-- An element `y` is in the ω-limit of `x` w.r.t. `f` if the forward
images of `x` frequently (w.r.t. `f`) falls within an arbitrary neighbourhood of `y`. -/
theorem mem_omegaLimit_singleton_iff_map_cluster_point (x : α) (y : β) :
    y ∈ ω f ϕ { x } ↔ MapClusterPt y f fun t ↦ ϕ t x := by
  simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff_frequently, singleton_inter_nonempty, mem_preimage]

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