Math 2.0

statement theorem

One-sided limits of a monotone function exist

Statement

Let a<c<ba < c < b and let f ⁣:(a,b)→Rf \colon (a, b) \to \mathbb{R} be increasing. Then both one-sided limits of ff at cc exist, and lim⁡x→c−f(x)=sup⁡a<x<cf(x)≤f(c)≤inf⁡c<x<bf(x)=lim⁡x→c+f(x).\lim_{x \to c^-} f(x) = \sup_{a < x < c} f(x) \le f(c) \le \inf_{c < x < b} f(x) = \lim_{x \to c^+} f(x).

Remarks

The proof is the same as for the monotone convergence theorem. The supremum exists because f(c)f(c) is an upper bound. A similar statement holds for decreasing functions, with the inequalities reversed. So ff is continuous at cc exactly when the two one-sided limits are equal. Otherwise cc is a jump discontinuity. Mathlib states the left limit as Monotone.tendsto_nhdsLT.

Explanations

L1 human

An increasing function can only move up as xx approaches cc from the left. Its values are bounded by f(c)f(c), so they settle at a limit.

What this node needs for W1
  • an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a node is. They do not measure its truth.

What this needs

To read this node, read these 10 nodes in this order. The foundations come first, and the list ends with this node.

Each node uses the nodes above it. The colour of the bar on a box shows the evidence level, and the box also gives it as text. The list below has the same nodes.
  • no evidence level
  1. Limit point of a set definition
  2. Sequence definition
  3. Limit of a function definition
  4. Real sequence definition
  5. One-sided limit definition
  6. Bounded sequence definition
  7. Limit of a sequence definition
  8. Monotone sequence definition
  9. Monotone convergence theorem for sequences statement
  10. One-sided limits of a monotone function exist statement

What depends on this

28 nodes use this node, directly or through other nodes.

Sources

  1. Web https://en.wikipedia.org/wiki/Monotonic_function, Some basic applications and results