Theory of topology on ordered spaces #
Main definitions #
The order topology on an ordered space is the topology generated by all open intervals (or
equivalently by those of the form (-∞, a)
and (b, +∞)
). We define it as preorder.topology α
.
However, we do not register it as an instance (as many existing ordered types already have
topologies, which would be equal but not definitionally equal to preorder.topology α
). Instead,
we introduce a class order_topology α
(which is a Prop
, also known as a mixin) saying that on
the type α
having already a topological space structure and a preorder structure, the topological
structure is equal to the order topology.
We also introduce another (mixin) class order_closed_topology α
saying that the set of points
(x, y)
with x ≤ y
is closed in the product space. This is automatically satisfied on a linear
order with the order topology.
We prove many basic properties of such topologies.
Main statements #
This file contains the proofs of the following facts. For exact requirements
(order_closed_topology
vs order_topology
, preorder
vs partial_order
vs linear_order
etc)
see their statements.
Open / closed sets #
is_open_lt
: iff
andg
are continuous functions, then{x | f x < g x}
is open;is_open_Iio
,is_open_Ioi
,is_open_Ioo
: open intervals are open;is_closed_le
: iff
andg
are continuous functions, then{x | f x ≤ g x}
is closed;is_closed_Iic
,is_closed_Ici
,is_closed_Icc
: closed intervals are closed;frontier_le_subset_eq
,frontier_lt_subset_eq
: frontiers of both{x | f x ≤ g x}
and{x | f x < g x}
are included by{x | f x = g x}
;exists_Ioc_subset_of_mem_nhds
,exists_Ico_subset_of_mem_nhds
: ifx < y
, then any neighborhood ofx
includes an interval[x, z)
for somez ∈ (x, y]
, and any neighborhood ofy
includes an interval(z, y]
for somez ∈ [x, y)
.
Convergence and inequalities #
le_of_tendsto_of_tendsto
: iff
converges toa
,g
converges tob
, and eventuallyf x ≤ g x
, thena ≤ b
le_of_tendsto
,ge_of_tendsto
: iff
converges toa
and eventuallyf x ≤ b
(resp.,b ≤ f x
), thena ≤ b
(resp.,b ≤ a); we also provide primed versions that assume the inequalities to hold for all
x`.
Min, max, Sup
and Inf
#
continuous.min
,continuous.max
: pointwisemin
/max
of two continuous functions is continuous.tendsto.min
,tendsto.max
: iff
tends toa
andg
tends tob
, then their pointwisemin
/max
tend tomin a b
andmax a b
, respectively.tendsto_of_tendsto_of_tendsto_of_le_of_le
: theorem known as squeeze theorem, sandwich theorem, theorem of Carabinieri, and two policemen (and a drunk) theorem; ifg
andh
both converge toa
, and eventuallyg x ≤ f x ≤ h x
, thenf
converges toa
.
Connected sets and Intermediate Value Theorem #
is_preconnected_I??
: all intervalsI??
are preconnected,is_preconnected.intermediate_value
,intermediate_value_univ
: Intermediate Value Theorem for connected sets and connected spaces, respectively;intermediate_value_Icc
,intermediate_value_Icc'
: Intermediate Value Theorem for functions on closed intervals.
Miscellaneous facts #
is_compact.exists_forall_le
,is_compact.exists_forall_ge
: extreme value theorem, a continuous function on a compact set takes its minimum and maximum values.is_closed.Icc_subset_of_forall_mem_nhds_within
: “Continuous induction” principle; ifs ∩ [a, b]
is closed,a ∈ s
, and for eachx ∈ [a, b) ∩ s
some of its right neighborhoods is includeds
, then[a, b] ⊆ s
.is_closed.Icc_subset_of_forall_exists_gt
,is_closed.mem_of_ge_of_forall_exists_gt
: two other versions of the “continuous induction” principle.
Implementation #
We do not register the order topology as an instance on a preorder (or even on a linear order).
Indeed, on many such spaces, a topology has already been constructed in a different way (think
of the discrete spaces ℕ
or ℤ
, or ℝ
that could inherit a topology as the completion of ℚ
),
and is in general not defeq to the one generated by the intervals. We make it available as a
definition preorder.topology α
though, that can be registered as an instance when necessary, or
for specific types.
A topology on a set which is both a topological space and a preorder is order-closed if the
set of points (x, y)
with x ≤ y
is closed in the product space. We introduce this as a mixin.
This property is satisfied for the order topology on a linear order, but it can be satisfied more
generally, and suffices to derive many interesting properties relating order and topology.
Equations
If s
is a closed set and two functions f
and g
are continuous on s
,
then the set {x ∈ s | f x ≤ g x}
is a closed set.
Intermediate value theorem for two functions: if f
and g
are two continuous functions
on a preconnected space and f a ≤ g a
and g b ≤ f b
, then for some x
we have f x = g x
.
Intermediate value theorem for two functions: if f
and g
are two functions continuous
on a preconnected set s
and for some a b ∈ s
we have f a ≤ g a
and g b ≤ f b
,
then for some x ∈ s
we have f x = g x
.
Intermediate Value Theorem for continuous functions on connected sets.
Intermediate Value Theorem for continuous functions on connected spaces.
Intermediate Value Theorem for continuous functions on connected spaces.
If a preconnected set contains endpoints of an interval, then it includes the whole interval.
If a preconnected set contains endpoints of an interval, then it includes the whole interval.
If preconnected set in a linear order space is unbounded below and above, then it is the whole space.
Neighborhoods to the left and to the right on an order_closed_topology
#
Limits to the left and to the right of real functions are defined in terms of neighborhoods to
the left and to the right, either open or closed, i.e., members of 𝓝[Ioi a] a
and
𝓝[Ici a] a
on the right, and similarly on the left. Here we simply prove that all
right-neighborhoods of a point are equal, and we'll prove later other useful characterizations which
require the stronger hypothesis order_topology α
Right neighborhoods, point excluded #
Left neighborhoods, point excluded #
Right neighborhoods, point included #
Left neighborhoods, point included #
- topology_eq_generate_intervals : t = topological_space.generate_from {s : set α | ∃ (a : α), s = set.Ioi a ∨ s = set.Iio a}
The order topology on an ordered type is the topology generated by open intervals. We register
it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed.
We define it as a mixin. If you want to introduce the order topology on a preorder, use
preorder.topology
.
(Order) topology on a partial order α
generated by the subbase of open intervals
(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b}
for all a, b
in α
. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary.
Equations
- preorder.topology α = topological_space.generate_from {s : set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}
Also known as squeeze or sandwich theorem. This version assumes that inequalities hold eventually for the filter.
Also known as squeeze or sandwich theorem. This version assumes that inequalities hold everywhere.
On an ord_connected
subset of a linear order, the order topology for the restriction of the
order is the same as the restriction to the subset of the order topology.
A set is a neighborhood of a
if and only if it contains an interval (l, u)
containing a
,
provided a
is neither a bottom element nor a top element.
A set is a neighborhood of a
if and only if it contains an interval (l, u)
containing a
.
Intervals in Π i, π i
belong to 𝓝 x
#
For each leamma pi_Ixx_mem_nhds
we add a non-dependent version pi_Ixx_mem_nhds'
because
sometimes Lean fails to unify different instances while trying to apply the dependent version to,
e.g., ι → ℝ
.
Neighborhoods to the left and to the right on an order_topology
#
We've seen some properties of left and right neighborhood of a point in an order_closed_topology
.
In an order_topology
, such neighborhoods can be characterized as the sets containing suitable
intervals to the right or to the left of a
. We give now these characterizations.
The following statements are equivalent:
s
is a neighborhood ofa
within(a, +∞)
s
is a neighborhood ofa
within(a, b]
s
is a neighborhood ofa
within(a, b)
s
includes(a, u)
for someu ∈ (a, b]
s
includes(a, u)
for someu > a
A set is a neighborhood of a
within (a, +∞)
if and only if it contains an interval (a, u)
with a < u < u'
, provided a
is not a top element.
A set is a neighborhood of a
within (a, +∞)
if and only if it contains an interval (a, u)
with a < u
.
A set is a neighborhood of a
within (a, +∞)
if and only if it contains an interval (a, u]
with a < u
.
The following statements are equivalent:
s
is a neighborhood ofb
within(-∞, b)
s
is a neighborhood ofb
within[a, b)
s
is a neighborhood ofb
within(a, b)
s
includes(l, b)
for somel ∈ [a, b)
s
includes(l, b)
for somel < b
A set is a neighborhood of a
within (-∞, a)
if and only if it contains an interval (l, a)
with l < a
, provided a
is not a bottom element.
A set is a neighborhood of a
within (-∞, a)
if and only if it contains an interval (l, a)
with l < a
.
A set is a neighborhood of a
within (-∞, a)
if and only if it contains an interval [l, a)
with l < a
.
The following statements are equivalent:
s
is a neighborhood ofa
within[a, +∞)
s
is a neighborhood ofa
within[a, b]
s
is a neighborhood ofa
within[a, b)
s
includes[a, u)
for someu ∈ (a, b]
s
includes[a, u)
for someu > a
A set is a neighborhood of a
within [a, +∞)
if and only if it contains an interval [a, u)
with a < u < u'
, provided a
is not a top element.
A set is a neighborhood of a
within [a, +∞)
if and only if it contains an interval [a, u)
with a < u
.
A set is a neighborhood of a
within [a, +∞)
if and only if it contains an interval [a, u]
with a < u
.
The following statements are equivalent:
s
is a neighborhood ofb
within(-∞, b]
s
is a neighborhood ofb
within[a, b]
s
is a neighborhood ofb
within(a, b]
s
includes(l, b]
for somel ∈ [a, b)
s
includes(l, b]
for somel < b
A set is a neighborhood of a
within (-∞, a]
if and only if it contains an interval (l, a]
with l < a
, provided a
is not a bottom element.
A set is a neighborhood of a
within (-∞, a]
if and only if it contains an interval (l, a]
with l < a
.
A set is a neighborhood of a
within (-∞, a]
if and only if it contains an interval [l, a]
with l < a
.
A set is a neighborhood of a
within [a, +∞)
if and only if it contains an interval [a, u]
with a < u
.
A set is a neighborhood of a
within (-∞, a]
if and only if it contains an interval [l, a]
with l < a
.
In a linearly ordered additive commutative group with the order topology, if f
tends to C
and g
tends to at_top
then f + g
tends to at_top
.
In a linearly ordered additive commutative group with the order topology, if f
tends to C
and g
tends to at_bot
then f + g
tends to at_bot
.
In a linearly ordered additive commutative group with the order topology, if f
tends to
at_top
and g
tends to C
then f + g
tends to at_top
.
In a linearly ordered additive commutative group with the order topology, if f
tends to
at_bot
and g
tends to C
then f + g
tends to at_bot
.
In a linearly ordered field with the order topology, if f
tends to at_top
and g
tends to
a positive constant C
then f * g
tends to at_top
.
In a linearly ordered field with the order topology, if f
tends to a positive constant C
and
g
tends to at_top
then f * g
tends to at_top
.
In a linearly ordered field with the order topology, if f
tends to at_top
and g
tends to
a negative constant C
then f * g
tends to at_bot
.
In a linearly ordered field with the order topology, if f
tends to a negative constant C
and
g
tends to at_top
then f * g
tends to at_bot
.
In a linearly ordered field with the order topology, if f
tends to at_bot
and g
tends to
a positive constant C
then f * g
tends to at_bot
.
In a linearly ordered field with the order topology, if f
tends to at_bot
and g
tends to
a negative constant C
then f * g
tends to at_top
.
In a linearly ordered field with the order topology, if f
tends to a positive constant C
and
g
tends to at_bot
then f * g
tends to at_bot
.
In a linearly ordered field with the order topology, if f
tends to a negative constant C
and
g
tends to at_bot
then f * g
tends to at_top
.
The function x ↦ x⁻¹
tends to +∞
on the right of 0
.
The function r ↦ r⁻¹
tends to 0
on the right as r → +∞
.
The function x^(-n)
tends to 0
at +∞
for any positive natural n
.
A version for positive real powers exists as tendsto_rpow_neg_at_top
.
Alias of is_lub.mem_of_is_closed
.
Alias of is_glb.mem_of_is_closed
.
A compact set is bounded below
A compact set is bounded above
The closure of the interval (a, +∞)
is the closed interval [a, +∞)
, unless a
is a top
element.
The closure of the interval (a, +∞)
is the closed interval [a, +∞)
.
The closure of the interval (-∞, a)
is the closed interval (-∞, a]
, unless a
is a bottom
element.
The closure of the interval (-∞, a)
is the interval (-∞, a]
.
The closure of the open interval (a, b)
is the closed interval [a, b]
.
The closure of the interval (a, b]
is the closed interval [a, b]
.
The closure of the interval [a, b)
is the closed interval [a, b]
.
The at_top
filter for an open interval Ioo a b
comes from the left-neighbourhoods filter at
the right endpoint in the ambient order.
The at_bot
filter for an open interval Ioo a b
comes from the right-neighbourhoods filter at
the left endpoint in the ambient order.
A monotone function continuous at the supremum of a nonempty set sends this supremum to the supremum of the image of this set.
A monotone function s
sending bot
to bot
and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set.
A monotone function continuous at the indexed supremum over a nonempty Sort
sends this indexed
supremum to the indexed supremum of the composition.
If a monotone function sending bot
to bot
is continuous at the indexed supremum over
a Sort
, then it sends this indexed supremum to the indexed supremum of the composition.
A monotone function continuous at the infimum of a nonempty set sends this infimum to the infimum of the image of this set.
A monotone function s
sending top
to top
and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set.
A monotone function continuous at the indexed infimum over a nonempty Sort
sends this indexed
infimum to the indexed infimum of the composition.
If a monotone function sending top
to top
is continuous at the indexed infimum over
a Sort
, then it sends this indexed infimum to the indexed infimum of the composition.
If a monotone function is continuous at the supremum of a nonempty bounded above set s
,
then it sends this supremum to the supremum of the image of s
.
If a monotone function is continuous at the indexed supremum of a bounded function on
a nonempty Sort
, then it sends this supremum to the supremum of the composition.
If a monotone function is continuous at the infimum of a nonempty bounded below set s
,
then it sends this infimum to the infimum of the image of s
.
A continuous monotone function sends indexed infimum to indexed infimum in conditionally complete linear order, under a boundedness assumption.
A bounded connected subset of a conditionally complete linear order includes the open interval
(Inf s, Sup s)
.
A preconnected set in a conditionally complete linear order is either one of the intervals
[Inf s, Sup s]
, [Inf s, Sup s)
, (Inf s, Sup s]
, (Inf s, Sup s)
, [Inf s, +∞)
,
(Inf s, +∞)
, (-∞, Sup s]
, (-∞, Sup s)
, (-∞, +∞)
, or ∅
. The converse statement requires
α
to be densely ordererd.
A preconnected set is either one of the intervals Icc
, Ico
, Ioc
, Ioo
, Ici
, Ioi
,
Iic
, Iio
, or univ
, or ∅
. The converse statement requires α
to be densely ordererd. Though
one can represent ∅
as (Inf s, Inf s)
, we include it into the list of possible cases to improve
readability.
A "continuous induction principle" for a closed interval: if a set s
meets [a, b]
on a closed subset, contains a
, and the set s ∩ [a, b)
has no maximal point, then b ∈ s
.
A "continuous induction principle" for a closed interval: if a set s
meets [a, b]
on a closed subset, contains a
, and for any a ≤ x < y ≤ b
, x ∈ s
, the set s ∩ (x, y]
is not empty, then [a, b] ⊆ s
.
A "continuous induction principle" for a closed interval: if a set s
meets [a, b]
on a closed subset, contains a
, and for any x ∈ s ∩ [a, b)
the set s
includes some open
neighborhood of x
within (x, +∞)
, then [a, b] ⊆ s
.
A closed interval in a densely ordered conditionally complete linear order is preconnected.
Alias of is_preconnected_iff_ord_connected
.
Alias of is_preconnected_iff_ord_connected
.
In a dense conditionally complete linear order, the set of preconnected sets is exactly
the set of the intervals Icc
, Ico
, Ioc
, Ioo
, Ici
, Ioi
, Iic
, Iio
, (-∞, +∞)
,
or ∅
. Though one can represent ∅
as (Inf s, Inf s)
, we include it into the list of
possible cases to improve readability.
Intermediate Value Theorem for continuous functions on closed intervals, case f a ≤ t ≤ f b
.
Intermediate Value Theorem for continuous functions on closed intervals, case f a ≥ t ≥ f b
.
Intermediate Value Theorem for continuous functions on closed intervals, unordered case.
A continuous function which tendsto at_top
at_top
and to at_bot
at_bot
is surjective.
A continuous function which tendsto at_bot
at_top
and to at_top
at_bot
is surjective.
If a function f : α → β
is continuous on a nonempty interval s
, its restriction to s
tends to at_bot : filter β
along at_bot : filter ↥s
and tends to at_top : filter β
along
at_top : filter ↥s
, then the restriction of f
to s
is surjective. We formulate the
conclusion as surj_on f s univ
.
If a function f : α → β
is continuous on a nonempty interval s
, its restriction to s
tends to at_top : filter β
along at_bot : filter ↥s
and tends to at_bot : filter β
along
at_top : filter ↥s
, then the restriction of f
to s
is surjective. We formulate the
conclusion as surj_on f s univ
.
A closed interval in a conditionally complete linear order is compact.
An unordered closed interval in a conditionally complete linear order is compact.
The extreme value theorem: a continuous function realizes its minimum on a compact set
The extreme value theorem: a continuous function realizes its maximum on a compact set
The extreme value theorem: if a continuous function f
tends to infinity away from compact
sets, then it has a global minimum.
The extreme value theorem: if a continuous function f
tends to negative infinity away from
compactx sets, then it has a global maximum.
If the liminf and the limsup of a filter coincide, then this filter converges to their common value, at least if the filter is eventually bounded above and below.
If a filter is converging, its limsup coincides with its limit.
If a filter is converging, its liminf coincides with its limit.
If a function has a limit, then its limsup coincides with its limit.
If a function has a limit, then its liminf coincides with its limit.
If the liminf and the limsup of a function coincide, then the limit of the function exists and has the same value
If a number a
is less than or equal to the liminf
of a function f
at some filter
and is greater than or equal to the limsup
of f
, then f
tends to a
along this filter.
Here is a counter-example to a version of the following with conditionally_complete_lattice α
.
Take α = [0, 1) → ℝ
with the natural lattice structure, ι = ℕ
. Put f n x = -x^n
. Then
⨆ n, f n = 0
while none of f n
is strictly greater than the constant function -0.5
.
Continuity of monotone functions #
In this section we prove the following fact: if f
is a monotone function on a neighborhood of a
and the image of this neighborhood is a neighborhood of f a
, then f
is continuous at a
, see
continuous_at_of_mono_incr_on_of_image_mem_nhds
, as well as several similar facts.
If f
is a function strictly monotonically increasing on a right neighborhood of a
and the
image of this neighborhood under f
meets every interval (f a, b]
, b > f a
, then f
is
continuous at a
from the right.
The assumption hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
is required because otherwise the
function f : ℝ → ℝ
given by f x = if x ≤ 0 then x else x + 1
would be a counter-example at
a = 0
.
If f
is a function monotonically increasing function on a right neighborhood of a
and the
image of this neighborhood under f
meets every interval (f a, b)
, b > f a
, then f
is
continuous at a
from the right.
The assumption hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
cannot be replaced by the weaker
assumption hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
we use for strictly monotone functions
because otherwise the function ceil : ℝ → ℤ
would be a counter-example at a = 0
.
If a function f
with a densely ordered codomain is monotonically increasing on a right
neighborhood of a
and the closure of the image of this neighborhood under f
is a right
neighborhood of f a
, then f
is continuous at a
from the right.
If a function f
with a densely ordered codomain is monotonically increasing on a right
neighborhood of a
and the image of this neighborhood under f
is a right neighborhood of f a
,
then f
is continuous at a
from the right.
If a function f
with a densely ordered codomain is strictly monotonically increasing on a
right neighborhood of a
and the closure of the image of this neighborhood under f
is a right
neighborhood of f a
, then f
is continuous at a
from the right.
If a function f
with a densely ordered codomain is strictly monotonically increasing on a
right neighborhood of a
and the image of this neighborhood under f
is a right neighborhood of
f a
, then f
is continuous at a
from the right.
If a function f
is strictly monotonically increasing on a right neighborhood of a
and the
image of this neighborhood under f
includes Ioi (f a)
, then f
is continuous at a
from the
right.
If f
is a function strictly monotonically increasing on a left neighborhood of a
and the
image of this neighborhood under f
meets every interval [b, f a)
, b < f a
, then f
is
continuous at a
from the left.
The assumption hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)
is required because otherwise the
function f : ℝ → ℝ
given by f x = if x < 0 then x else x + 1
would be a counter-example at
a = 0
.
If f
is a function monotonically increasing function on a left neighborhood of a
and the
image of this neighborhood under f
meets every interval (b, f a)
, b < f a
, then f
is
continuous at a
from the left.
The assumption hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)
cannot be replaced by the weaker
assumption hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)
we use for strictly monotone functions
because otherwise the function floor : ℝ → ℤ
would be a counter-example at a = 0
.
If a function f
with a densely ordered codomain is monotonically increasing on a left
neighborhood of a
and the closure of the image of this neighborhood under f
is a left
neighborhood of f a
, then f
is continuous at a
from the left
If a function f
with a densely ordered codomain is monotonically increasing on a left
neighborhood of a
and the image of this neighborhood under f
is a left neighborhood of f a
,
then f
is continuous at a
from the left.
If a function f
with a densely ordered codomain is strictly monotonically increasing on a
left neighborhood of a
and the closure of the image of this neighborhood under f
is a left
neighborhood of f a
, then f
is continuous at a
from the left.
If a function f
with a densely ordered codomain is strictly monotonically increasing on a
left neighborhood of a
and the image of this neighborhood under f
is a left neighborhood of
f a
, then f
is continuous at a
from the left.
If a function f
is strictly monotonically increasing on a left neighborhood of a
and the
image of this neighborhood under f
includes Iio (f a)
, then f
is continuous at a
from the
left.
If a function f
is strictly monotonically increasing on a neighborhood of a
and the image of
this neighborhood under f
meets every interval [b, f a)
, b < f a
, and every interval
(f a, b]
, b > f a
, then f
is continuous at a
.
If a function f
with a densely ordered codomain is strictly monotonically increasing on a
neighborhood of a
and the closure of the image of this neighborhood under f
is a neighborhood of
f a
, then f
is continuous at a
.
If a function f
with a densely ordered codomain is strictly monotonically increasing on a
neighborhood of a
and the image of this set under f
is a neighborhood of f a
, then f
is
continuous at a
.
If f
is a function monotonically increasing function on a neighborhood of a
and the image of
this neighborhood under f
meets every interval (b, f a)
, b < f a
, and every interval (f a, b)
, b > f a
, then f
is continuous at a
.
If a function f
with a densely ordered codomain is monotonically increasing on a neighborhood
of a
and the closure of the image of this neighborhood under f
is a neighborhood of f a
, then
f
is continuous at a
.
If a function f
with a densely ordered codomain is monotonically increasing on a neighborhood
of a
and the image of this neighborhood under f
is a neighborhood of f a
, then f
is
continuous at a
.
A monotone function with densely ordered codomain and a dense range is continuous.
A monotone surjective function with a densely ordered codomain is surjective.
Continuity of order isomorphisms #
In this section we prove that an order_iso
is continuous, hence it is a homeomorph
. We prove
this for an order_iso
between to partial orders with order topology.
An order isomorphism between two linear order order_topology
spaces is a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := e.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}