Bounded monotone sequences converge #
In this file we prove a few theorems of the form “if the range of a monotone function f : ι → α
admits a least upper bound a
, then f x
tends to a
as x → ∞
”, as well as version of this
statement for (conditionally) complete lattices that use ⨆ x, f x
instead of IsLUB
.
These theorems work for linear orders with order topologies as well as their products (both in terms
of Prod
and in terms of function types). In order to reduce code duplication, we introduce two
typeclasses (one for the property formulated above and one for the dual property), prove theorems
assuming one of these typeclasses, and provide instances for linear orders and their products.
We also prove some "inverse" results: if f n
is a monotone sequence and a
is its limit,
then f n ≤ a
for all n
.
Tags #
monotone convergence
We say that α
is a SupConvergenceClass
if the following holds. Let f : ι → α
be a
monotone function, let a : α
be a least upper bound of Set.range f
. Then f x
tends to 𝓝 a
as x → ∞
(formally, at the filter Filter.atTop
). We require this for ι = (s : Set α)
,
f = CoeTC.coe
in the definition, then prove it for any f
in tendsto_atTop_isLUB
.
This property holds for linear orders with order topology as well as their products.
- tendsto_coe_atTop_isLUB : ∀ (a : α) (s : Set α), IsLUB s a → Filter.Tendsto CoeTC.coe Filter.atTop (nhds a)
proof that a monotone function tends to
𝓝 a
asx → ∞
Instances
We say that α
is an InfConvergenceClass
if the following holds. Let f : ι → α
be a
monotone function, let a : α
be a greatest lower bound of Set.range f
. Then f x
tends to 𝓝 a
as x → -∞
(formally, at the filter Filter.atBot
). We require this for ι = (s : Set α)
,
f = CoeTC.coe
in the definition, then prove it for any f
in tendsto_atBot_isGLB
.
This property holds for linear orders with order topology as well as their products.
- tendsto_coe_atBot_isGLB : ∀ (a : α) (s : Set α), IsGLB s a → Filter.Tendsto CoeTC.coe Filter.atBot (nhds a)
proof that a monotone function tends to
𝓝 a
asx → -∞
Instances
The next family of results, such as isLUB_of_tendsto_atTop
and iSup_eq_of_tendsto
, are
converses to the standard fact that bounded monotone functions converge. They state, that if a
monotone function f
tends to a
along Filter.atTop
, then that value a
is a least upper bound
for the range of f
.
Related theorems above (IsLUB.isLUB_of_tendsto
, IsGLB.isGLB_of_tendsto
etc) cover the case
when f x
tends to a
as x
tends to some point b
in the domain.