# 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.

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

Equations

- Function.leftLim f a = if nhdsWithin a (Set.Iio a) = ⊥ ∨ ¬∃ (y : β), Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds y) then f a else limUnder (nhdsWithin a (Set.Iio a)) f

Instances For

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

Equations

- Function.rightLim f a = Function.leftLim f a

Instances For

source
theorem leftLim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [hα : TopologicalSpace α] [h'α : OrderTopology α] [T2Space β] {f : α → β} {a : α} {y : β} (h : nhdsWithin a (Set.Iio a) ≠ ⊥) (h' : Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds y)) :
Function.leftLim f a = y
source
theorem leftLim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {a : α} (h : nhdsWithin a (Set.Iio a) = ⊥) :
Function.leftLim f a = f a
source
theorem rightLim_eq_of_tendsto {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] [T2Space β] {f : α → β} {a : α} {y : β} (h : nhdsWithin a (Set.Ioi a) ≠ ⊥) (h' : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds y)) :
Function.rightLim f a = y
source
theorem rightLim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : α → β) {a : α} (h : nhdsWithin a (Set.Ioi a) = ⊥) :
Function.rightLim f a = f a
source
theorem Monotone.leftLim_eq_sSup {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x : α} [TopologicalSpace α] [OrderTopology α] (h : nhdsWithin x (Set.Iio x) ≠ ⊥) :
Function.leftLim f x = sSup (f '' Set.Iio x)
source
theorem Monotone.rightLim_eq_sInf {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x : α} [TopologicalSpace α] [OrderTopology α] (h : nhdsWithin x (Set.Ioi x) ≠ ⊥) :
Function.rightLim f x = sInf (f '' Set.Ioi x)
source
theorem Monotone.leftLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} (h : x ≤ y) :
Function.leftLim f x ≤ f y
source
theorem Monotone.le_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} (h : x < y) :
f x ≤ Function.leftLim f y
source
theorem Monotone.leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) :
Monotone (Function.leftLim f)
source
theorem Monotone.le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} (h : x ≤ y) :
f x ≤ Function.rightLim f y
source
theorem Monotone.rightLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} (h : x < y) :
Function.rightLim f x ≤ f y
source
theorem Monotone.rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) :
Monotone (Function.rightLim f)
source
theorem Monotone.leftLim_le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} (h : x ≤ y) :
Function.leftLim f x ≤ Function.rightLim f y
source
theorem Monotone.rightLim_le_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} (h : x < y) :
Function.rightLim f x ≤ Function.leftLim f y
source
theorem Monotone.tendsto_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))
source
theorem Monotone.tendsto_leftLim_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhdsWithin (Function.leftLim f x) (Set.Iic (Function.leftLim f x)))
source
theorem Monotone.tendsto_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))
source
theorem Monotone.tendsto_rightLim_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhdsWithin (Function.rightLim f x) (Set.Ici (Function.rightLim f x)))
source
theorem Monotone.continuousWithinAt_Iio_iff_leftLim_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x : α} [TopologicalSpace α] [OrderTopology α] :
ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f 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.

source
theorem Monotone.continuousWithinAt_Ioi_iff_rightLim_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x : α} [TopologicalSpace α] [OrderTopology α] :
ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f 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.

source
theorem Monotone.continuousAt_iff_leftLim_eq_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x : α} [TopologicalSpace α] [OrderTopology α] :
ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x

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

source
theorem Antitone.le_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x y : α} (h : x ≤ y) :
f y ≤ Function.leftLim f x
source
theorem Antitone.leftLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x y : α} (h : x < y) :
Function.leftLim f y ≤ f x
source
theorem Antitone.leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) :
Antitone (Function.leftLim f)
source
theorem Antitone.rightLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x y : α} (h : x ≤ y) :
Function.rightLim f y ≤ f x
source
theorem Antitone.le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x y : α} (h : x < y) :
f y ≤ Function.rightLim f x
source
theorem Antitone.rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) :
Antitone (Function.rightLim f)
source
theorem Antitone.rightLim_le_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x y : α} (h : x ≤ y) :
Function.rightLim f y ≤ Function.leftLim f x
source
theorem Antitone.leftLim_le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x y : α} (h : x < y) :
Function.leftLim f y ≤ Function.rightLim f x
source
theorem Antitone.tendsto_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))
source
theorem Antitone.tendsto_leftLim_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhdsWithin (Function.leftLim f x) (Set.Ici (Function.leftLim f x)))
source
theorem Antitone.tendsto_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (Function.rightLim f x))
source
theorem Antitone.tendsto_rightLim_within {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) [TopologicalSpace α] [OrderTopology α] (x : α) :
Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhdsWithin (Function.rightLim f x) (Set.Iic (Function.rightLim f x)))
source
theorem Antitone.continuousWithinAt_Iio_iff_leftLim_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x : α} [TopologicalSpace α] [OrderTopology α] :
ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f 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.

source
theorem Antitone.continuousWithinAt_Ioi_iff_rightLim_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x : α} [TopologicalSpace α] [OrderTopology α] :
ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f 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.

source
theorem Antitone.continuousAt_iff_leftLim_eq_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) {x : α} [TopologicalSpace α] [OrderTopology α] :
ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x

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