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 : if f and g 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 : if f and g 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 : if x < y, then any neighborhood of x includes an interval [x, z) for some z ∈ (x, y], and any neighborhood of y includes an interval (z, y] for some z ∈ [x, y).

Convergence and inequalities #

• le_of_tendsto_of_tendsto : if f converges to a, g converges to b, and eventually f x ≤ g x, then a ≤ b
• le_of_tendsto, ge_of_tendsto : if f converges to a and eventually f x ≤ b (resp., b ≤ f x), then a ≤ b (resp., b ≤ a); we also provide primed versions that assume the inequalities to hold for allx`.

Min, max, Sup and Inf #

• continuous.min, continuous.max: pointwise min/max of two continuous functions is continuous.
• tendsto.min, tendsto.max : if f tends to a and g tends to b, then their pointwise min/max tend to min a b and max 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; if g and h both converge to a, and eventually g x ≤ f x ≤ h x, then f converges to a.

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.

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 𝓝[>] a and 𝓝[≥] 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 #

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., ι → ℝ.