mathlib documentation

topology.algebra.order.left_right_lim

Left and right limits #

We define the (strict) left and right limits of a function.

We develop a comprehensive API for monotone functions. Notably,

We also port the API to antitone functions.

TODO #

Prove corresponding stronger results for strict_mono and strict_anti functions.

@[irreducible]
noncomputable def function.left_lim {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space β] (f : α β) (a : α) :
β

Let f : α → β be a function from a linear order α to a topological_space β, and let a : α. The limit strictly to the left of f at a, denoted with left_lim f a, is defined by using the order topology on α. If a is isolated to its left or the function has no left limit, we use f a instead to guarantee a good behavior in most cases.

Equations
noncomputable def function.right_lim {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space β] (f : α β) (a : α) :
β

Let f : α → β be a function from a linear order α to a topological_space β, and let a : α. The limit strictly to the right of f at a, denoted with right_lim f a, is defined by using the order topology on α. If a is isolated to its right or the function has no right limit, , we use f a instead to guarantee a good behavior in most cases.

Equations
theorem left_lim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space β] [hα : topological_space α] [h'α : order_topology α] [t2_space β] {f : α β} {a : α} {y : β} (h : nhds_within a (set.Iio a) ) (h' : filter.tendsto f (nhds_within a (set.Iio a)) (nhds y)) :
theorem left_lim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space β] [hα : topological_space α] [h'α : order_topology α] (f : α β) {a : α} (h : nhds_within a (set.Iio a) = ) :
theorem monotone.left_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : monotone f) {x y : α} (h : x y) :
theorem monotone.le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : monotone f) {x y : α} (h : x < y) :
@[protected]
theorem monotone.le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : monotone f) {x y : α} (h : x y) :
theorem monotone.right_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : monotone f) {x y : α} (h : x < y) :
@[protected]
theorem monotone.left_lim_le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : monotone f) {x y : α} (h : x y) :
theorem monotone.right_lim_le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : monotone f) {x y : α} (h : x < y) :

A monotone function is continuous to the left at a point if and only if its left limit coincides with the value of the function.

A monotone function is continuous to the right at a point if and only if its right limit coincides with the value of the function.

A monotone function is continuous at a point if and only if its left and right limits coincide.

In a second countable space, the set of points where a monotone function is not right-continuous is at most countable. Superseded by countable_not_continuous_at which gives the two-sided version.

In a second countable space, the set of points where a monotone function is not left-continuous is at most countable. Superseded by countable_not_continuous_at which gives the two-sided version.

In a second countable space, the set of points where a monotone function is not continuous is at most countable.

theorem antitone.le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : antitone f) {x y : α} (h : x y) :
theorem antitone.left_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : antitone f) {x y : α} (h : x < y) :
@[protected]
theorem antitone.right_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : antitone f) {x y : α} (h : x y) :
theorem antitone.le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : antitone f) {x y : α} (h : x < y) :
@[protected]
theorem antitone.right_lim_le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : antitone f) {x y : α} (h : x y) :
theorem antitone.left_lim_le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] {f : α β} (hf : antitone f) {x y : α} (h : x < y) :

An antitone function is continuous to the left at a point if and only if its left limit coincides with the value of the function.

An antitone function is continuous to the right at a point if and only if its right limit coincides with the value of the function.

An antitone function is continuous at a point if and only if its left and right limits coincide.

In a second countable space, the set of points where an antitone function is not continuous is at most countable.