# mathlib3documentation

topology.algebra.order.left_right_lim

# Left and right limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

• left_lim f x is the strict left limit of f at x (using f x as a garbage value if x is isolated to its left).
• right_lim f x is the strict right limit of f at x (using f x as a garbage value if x is isolated to its right).

We develop a comprehensive API for monotone functions. Notably,

• monotone.continuous_at_iff_left_lim_eq_right_lim states that a monotone function is continuous at a point if and only if its left and right limits coincide.
• monotone.countable_not_continuous_at asserts that a monotone function taking values in a second-countable space has at most countably many discontinuity points.

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 α] (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 α] (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 α] [hα : topological_space α] [h'α : order_topology α] [t2_space β] {f : α β} {a : α} {y : β} (h : (set.Iio a) ) (h' : (set.Iio a)) (nhds y)) :
= y
theorem left_lim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [linear_order α] [hα : topological_space α] [h'α : order_topology α] (f : α β) {a : α} (h : (set.Iio a) = ) :
= f a
theorem monotone.left_lim_eq_Sup {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x : α} (h : (set.Iio x) ) :
theorem monotone.left_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x y : α} (h : x y) :
f y
theorem monotone.le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x y : α} (h : x < y) :
f x
@[protected]
theorem monotone.left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) :
theorem monotone.le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x y : α} (h : x y) :
f x
theorem monotone.right_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x y : α} (h : x < y) :
f y
@[protected]
theorem monotone.right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) :
theorem monotone.left_lim_le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x y : α} (h : x y) :
theorem monotone.right_lim_le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x y : α} (h : x < y) :
theorem monotone.tendsto_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) (x : α) :
(set.Iio x)) (nhds x))
theorem monotone.tendsto_left_lim_within {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) (x : α) :
(set.Iio x)) (nhds_within x) (set.Iic x)))
theorem monotone.tendsto_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) (x : α) :
(set.Ioi x)) (nhds x))
theorem monotone.tendsto_right_lim_within {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) (x : α) :
(set.Ioi x)) (set.Ici x)))
theorem monotone.continuous_within_at_Iio_iff_left_lim_eq {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x : α}  :
x = f x

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.

theorem monotone.continuous_within_at_Ioi_iff_right_lim_eq {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x : α}  :
x = f x

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.

theorem monotone.continuous_at_iff_left_lim_eq_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f) {x : α}  :

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

theorem monotone.countable_not_continuous_within_at_Ioi {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f)  :
{x : α | ¬ x}.countable

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.

theorem monotone.countable_not_continuous_within_at_Iio {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f)  :
{x : α | ¬ x}.countable

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.

theorem monotone.countable_not_continuous_at {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : monotone f)  :
{x : α | ¬ x}.countable

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 α] {f : α β} (hf : antitone f) {x y : α} (h : x y) :
f y
theorem antitone.left_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x y : α} (h : x < y) :
f x
@[protected]
theorem antitone.left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) :
theorem antitone.right_lim_le {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x y : α} (h : x y) :
f x
theorem antitone.le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x y : α} (h : x < y) :
f y
@[protected]
theorem antitone.right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) :
theorem antitone.right_lim_le_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x y : α} (h : x y) :
theorem antitone.left_lim_le_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x y : α} (h : x < y) :
theorem antitone.tendsto_left_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) (x : α) :
(set.Iio x)) (nhds x))
theorem antitone.tendsto_left_lim_within {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) (x : α) :
(set.Iio x)) (nhds_within x) (set.Ici x)))
theorem antitone.tendsto_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) (x : α) :
(set.Ioi x)) (nhds x))
theorem antitone.tendsto_right_lim_within {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) (x : α) :
(set.Ioi x)) (set.Iic x)))
theorem antitone.continuous_within_at_Iio_iff_left_lim_eq {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x : α}  :
x = f x

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.

theorem antitone.continuous_within_at_Ioi_iff_right_lim_eq {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x : α}  :
x = f x

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.

theorem antitone.continuous_at_iff_left_lim_eq_right_lim {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f) {x : α}  :

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

theorem antitone.countable_not_continuous_at {α : Type u_1} {β : Type u_2} [linear_order α] {f : α β} (hf : antitone f)  :
{x : α | ¬ x}.countable

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