Math 2.0

Real functions Theorem

Boundedness theorem

Builds on Continuous functionBolzano–Weierstrass theorem

Statement

Let a≤ba \le b and let f ⁣:[a,b]→ℝf \colon [a, b] \to \mathbb{R} be continuous. Then ff is bounded. That is, there is KK with ∣f(x)∣≤K|f(x)| \le K for all x∈[a,b]x \in [a, b].

Remarks

Suppose not. Then there are points xn∈[a,b]x_n \in [a, b] with ∣f(xn)∣>n|f(x_n)| > n. By the Bolzano–Weierstrass theorem, a subsequence converges to some c∈[a,b]c \in [a, b]. Continuity at cc gives a contradiction. The interval must be closed and bounded. The function 1/x1/x on (0,1](0, 1] is continuous but not bounded. Mathlib states a form for compact sets, as IsCompact.bddAbove_image.

Reading path

To understand this page from the ground up, read these 15 pages in order. The foundations come first.

Show the path as a graph
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Limit point of a set definition
  2. Sequence definition
  3. Limit of a function definition
  4. Real sequence definition
  5. Subsequence definition
  6. Continuity at a point definition
  7. Bounded sequence definition
  8. Limit of a sequence definition
  9. Monotone sequence definition
  10. Continuous function definition
  11. Convergent sequence definition
  12. Monotone convergence theorem for sequences statement
  13. Every sequence has a monotone subsequence statement
  14. Bolzano–Weierstrass theorem statement
  15. Boundedness theorem statement

Where this leads

122 pages build on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Extreme_value_theorem, Proof of the boundedness theorem
About this page
Tag0ATVXC3NCC
URIm2://0ATVXC3NCC
Kindstatement, theorem
WritingW0 stub
MSC26A15
StatusThis copy of the site has no build data. Run m2 status 0ATVXC3NCC.
UsesContinuous function, Bolzano–Weierstrass theorem

Markdown · JSON · Edit on GitHub

What this page 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 page is. They do not measure its truth.

What links here

Used by