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 OrderTopology α (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 prove many basic properties of such topologies.
Main statements #
This file contains the proofs of the following facts. For exact requirements
(OrderClosedTopology vs OrderTopology, Preorder vs PartialOrder vs LinearOrder etc)
see their statements.
exists_Ioc_subset_of_mem_nhds,exists_Ico_subset_of_mem_nhds: ifx < y, then any neighborhood ofxincludes an interval[x, z)for somez ∈ (x, y], and any neighborhood ofyincludes an interval(z, y]for somez ∈ [x, y).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; ifgandhboth converge toa, and eventuallyg x ≤ f x ≤ h x, thenfconverges toa.
Implementation notes #
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.
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.
Instances
(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 α = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}
Instances For
Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold eventually for the filter.
Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold everywhere.
The topology induced by a strictly monotone function with order-connected range is the preorder topology.
A strictly monotone function between linear orders with order topology is a topological
embedding provided that the range of f is order-connected.
Alias of StrictMono.isEmbedding_of_ordConnected.
A strictly monotone function between linear orders with order topology is a topological
embedding provided that the range of f is order-connected.
On a Set.OrdConnected 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 in a nontrivial densely linear ordered type is dense in the sense of topology if and only
if for any a < b there exists c ∈ s, a < c < b. Each implication requires less typeclass
assumptions.
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.
Let α be a densely ordered linear order with order topology. If α is a separable space, then
it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see
double arrow space for a counterexample.
The set of points which are isolated on the right is countable when the space is second-countable.
The set of points which are isolated on the left is countable when the space is second-countable.
The set of points which are isolated on the left is countable when the space is second-countable.
Consider a disjoint family of intervals (x, y) with x < y in a second-countable space.
Then the family is countable.
This is not a straightforward consequence of second-countability as some of these intervals might be
empty (but in fact this can happen only for countably many of them).
For a function taking values in a second countable space, the set of points x for
which the image under f of (x, ∞) is separated above from f x is countable.
For a function taking values in a second countable space, the set of points x for
which the image under f of (x, ∞) is separated below from f x is countable.
For a function taking values in a second countable space, the set of points x for
which the image under f of (-∞, x) is separated above from f x is countable.
For a function taking values in a second countable space, the set of points x for
which the image under f of (-∞, x) is separated below from f x is countable.
Intervals in Π i, π i belong to 𝓝 x #
For each lemma 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., ι → ℝ.