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} [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

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

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

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

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

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

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)

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)

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

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

theorem Monotone.leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) : Monotone (Function.leftLim f)

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

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

theorem Monotone.rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) : Monotone (Function.rightLim f)

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

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

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))

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)))

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))

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)))

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.

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.

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.

theorem Monotone.countable_not_continuousWithinAt_Ioi {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology β] : {x : α | ¬ContinuousWithinAt f (Set.Ioi 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_continuousAt which gives the two-sided version.

theorem Monotone.countable_not_continuousWithinAt_Iio {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology β] : {x : α | ¬ContinuousWithinAt f (Set.Iio 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_continuousAt which gives the two-sided version.

theorem Monotone.countable_not_continuousAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Monotone f) [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology β] : {x : α | ¬ContinuousAt f 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_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

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

theorem Antitone.leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) : Antitone (Function.leftLim f)

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

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

theorem Antitone.rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) : Antitone (Function.rightLim f)

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

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

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))

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)))

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))

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)))

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.

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.

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.

theorem Antitone.countable_not_continuousAt {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : Antitone f) [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology β] : {x : α | ¬ContinuousAt f x}.Countable

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