ω-limits #
For a function ϕ : τ → α → β
where β
is a topological space, we
define the ω-limit under ϕ
of a set s
in α
with respect to
filter f
on τ
: an element y : β
is in the ω-limit of s
if the
forward images of s
intersect arbitrarily small neighbourhoods of
y
frequently "in the direction of f
".
In practice ϕ
is often a continuous monoid-act, but the definition
requires only that ϕ
has a coercion to the appropriate function
type. In the case where τ
is ℕ
or ℝ
and f
is at_top
, we
recover the usual definition of the ω-limit set as the set of all y
such that there exist sequences (tₙ)
, (xₙ)
such that ϕ tₙ xₙ ⟶ y
as n ⟶ ∞
.
Notations #
The omega_limit
locale provides the localised notation ω
for
omega_limit
, as well as ω⁺
and ω⁻
for omega_limit at_top
and
omega_limit at_bot
respectively for when the acting monoid is
endowed with an order.
Definition and notation #
The ω-limit of a set s
under ϕ
with respect to a filter f
is
⋂ u ∈ f, cl (ϕ u s).
Equations
- omega_limit f ϕ s = ⋂ (u : set τ) (H : u ∈ f), closure (set.image2 ϕ u s)
Elementary properties #
Equivalent definitions of the omega limit #
The next few lemmas are various versions of the property characterising ω-limits:
An element y
is in the ω-limit set of s
w.r.t. f
if the
preimages of an arbitrary neighbourhood of y
frequently
(w.r.t. f
) intersects of s
.
An element y
is in the ω-limit set of s
w.r.t. f
if the
forward images of s
frequently (w.r.t. f
) intersect arbitrary
neighbourhoods of y
.
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
.
Set operations and omega limits #
Different expressions for omega limits, useful for rewrites. In
particular, one may restrict the intersection to sets in f
which are
subsets of some set v
also in f
.
`ω-limits and compactness #
A set is eventually carried into any open neighbourhood of its ω-limit:
if c
is a compact set such that closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c
for some v ∈ f
and n
is an open neighbourhood of ω f ϕ s
, then for some u ∈ f
we have
closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n
.
A set is eventually carried into any open neighbourhood of its ω-limit:
if c
is a compact set such that closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c
for some v ∈ f
and n
is an open neighbourhood of ω f ϕ s
, then for some u ∈ f
we have
closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n
.
The ω-limit of a nonempty set w.r.t. a nontrivial filter is nonempty.
ω-limits of Flows by a Monoid #
ω-limits of Flows by a Group #
the ω-limit of a forward image of s
is the same as the ω-limit of s
.