# Documentation

Mathlib.Topology.Algebra.Order.LeftRightLim

# Left and right limits #

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

• leftLim 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).
• rightLim 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.continuousAt_iff_leftLim_eq_rightLim states that a monotone function is continuous at a point if and only if its left and right limits coincide.
• Monotone.countable_not_continuousAt 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 StrictMono and StrictAnti functions.

noncomputable def Function.leftLim {α : Type u_1} {β : Type u_2} [] [] (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 leftLim 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.

Instances For
noncomputable def Function.rightLim {α : Type u_1} {β : Type u_2} [] [] (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 rightLim 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.

Instances For
theorem leftLim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [] [] [hα : ] [h'α : ] [] {f : αβ} {a : α} {y : β} (h : nhdsWithin a () ) (h' : Filter.Tendsto f (nhdsWithin a ()) (nhds y)) :
= y
theorem leftLim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [] [] [hα : ] [h'α : ] (f : αβ) {a : α} (h : nhdsWithin a () = ) :
= f a
theorem rightLim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {a : α} {y : β} (h : nhdsWithin a () ) (h' : Filter.Tendsto f (nhdsWithin a ()) (nhds y)) :
= y
theorem rightLim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [] [] [] [] (f : αβ) {a : α} (h : nhdsWithin a () = ) :
= f a
theorem Monotone.leftLim_eq_sSup {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} [] [] (h : nhdsWithin x () ) :
= sSup (f '' )
theorem Monotone.rightLim_eq_sInf {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} [] [] (h : nhdsWithin x () ) :
= sInf (f '' )
theorem Monotone.leftLim_le {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x y) :
f y
theorem Monotone.le_leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x < y) :
f x
theorem Monotone.leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
theorem Monotone.le_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x y) :
f x
theorem Monotone.rightLim_le {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x < y) :
f y
theorem Monotone.rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
theorem Monotone.leftLim_le_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x y) :
theorem Monotone.rightLim_le_leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x < y) :
theorem Monotone.tendsto_leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Monotone.tendsto_leftLim_within {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Monotone.tendsto_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Monotone.tendsto_rightLim_within {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Monotone.continuousWithinAt_Iio_iff_leftLim_eq {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {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.continuousWithinAt_Ioi_iff_rightLim_eq {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {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.continuousAt_iff_leftLim_eq_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} [] [] :

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

theorem Monotone.countable_not_continuousWithinAt_Ioi {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] :

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_continuousAt which gives the two-sided version.

theorem Monotone.countable_not_continuousWithinAt_Iio {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] :

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_continuousAt which gives the two-sided version.

theorem Monotone.countable_not_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] :

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

theorem Antitone.le_leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x y) :
f y
theorem Antitone.leftLim_le {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x < y) :
f x
theorem Antitone.leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
theorem Antitone.rightLim_le {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x y) :
f x
theorem Antitone.le_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x < y) :
f y
theorem Antitone.rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) :
theorem Antitone.rightLim_le_leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x y) :
theorem Antitone.leftLim_le_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} {y : α} (h : x < y) :
theorem Antitone.tendsto_leftLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Antitone.tendsto_leftLim_within {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Antitone.tendsto_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Antitone.tendsto_rightLim_within {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] (x : α) :
theorem Antitone.continuousWithinAt_Iio_iff_leftLim_eq {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {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.continuousWithinAt_Ioi_iff_rightLim_eq {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {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.continuousAt_iff_leftLim_eq_rightLim {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) {x : α} [] [] :

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

theorem Antitone.countable_not_continuousAt {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : ) [] [] :

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