Documentation

Mathlib.Topology.Order.LeftRightLim

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 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
Instances For
    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
    Instances For
      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)) :
      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) = ) :
      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)) :
      theorem rightLim_eq_of_eq_bot {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace β] [TopologicalSpace α] [OrderTopology α] (f : αβ) {a : α} (h : nhdsWithin a (Set.Ioi 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) ) :
      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) ) :
      theorem Monotone.leftLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Monotone f) {x : α} {y : α} (h : x y) :
      theorem Monotone.le_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Monotone f) {x : α} {y : α} (h : x < y) :
      theorem Monotone.le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Monotone f) {x : α} {y : α} (h : x y) :
      theorem Monotone.rightLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Monotone f) {x : α} {y : α} (h : x < y) :
      theorem Monotone.leftLim_le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Monotone f) {x : α} {y : α} (h : x 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) :

      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_continuousAt 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_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) :
      theorem Antitone.leftLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Antitone f) {x : α} {y : α} (h : x < y) :
      theorem Antitone.rightLim_le {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Antitone f) {x : α} {y : α} (h : x y) :
      theorem Antitone.le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Antitone f) {x : α} {y : α} (h : x < y) :
      theorem Antitone.rightLim_le_leftLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : Antitone f) {x : α} {y : α} (h : x y) :
      theorem Antitone.leftLim_le_rightLim {α : Type u_1} {β : Type u_2} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {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.

      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.