Math 2.0

Real functions Theorem

A continuous injective function on an interval is strictly monotone

Builds on Intermediate value theoremStrictly monotone function

Statement

Let II be an interval and let f ⁣:I→ℝf \colon I \to \mathbb{R} be continuous and injective. Then ff is strictly monotone.

Remarks

Suppose x<y<zx < y < z in II with f(y)f(y) not between f(x)f(x) and f(z)f(z). Then the intermediate value theorem gives a value of ff taken twice, which contradicts injectivity. Continuity is needed. The function on [0,2][0, 2] with f(x)=xf(x) = x for x<1x < 1 and f(x)=3−xf(x) = 3 - x for x≥1x \ge 1 is injective but not monotone. Mathlib states a form for closed intervals as ContinuousOn.strictMonoOn_of_injOn_Icc.

Reading path

To understand this page from the ground up, read these 7 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. Strictly monotone function definition
  3. Limit of a function definition
  4. Continuity at a point definition
  5. Continuous function definition
  6. Intermediate value theorem statement
  7. A continuous injective function on an interval is strictly monotone statement

Further reading

  1. Web https://en.wikipedia.org/wiki/Monotonic_function, Inverse of function
About this page
Tag0D6FCW80A0
URIm2://0D6FCW80A0
Kindstatement, theorem
WritingW0 stub
MSC26A48
StatusThis copy of the site has no build data. Run m2 status 0D6FCW80A0.
UsesIntermediate value theorem, Strictly monotone function

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

No page links to this page yet.