TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f[I]$ , and the inverse $g : f[I] \to I$ is continuous and strictly monotone in the same sense as $f$

Statement

Let $I \subseteq \mathbb{R}$ be order-convex (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length) and let $f : I \to \mathbb{R}$ be continuous on $I$ (Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$ : the $\varepsilon$ - $\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point) and injective (Injection, surjection, bijection). Then:

$f$ is strictly monotone (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$ , with the dictionary to monotone sequences);
$f[I]$ is order-convex;
the map $f : I \to f[I]$ is a bijection, so there is exactly one $g : f[I] \to I$ with $g(f(x)) = x$ for every $x \in I$ and $f(g(u)) = u$ for every $u \in f[I]$ ;
$g$ is strictly monotone in the same sense as $f$ : increasing if $f$ is increasing, decreasing if $f$ is decreasing;
$g$ is continuous on $f[I]$ .

"Interval" means "order-convex" here, as throughout this library (A subset of $\mathbb{R}$ is connected if and only if it is order-convex, that is, an interval is what licenses the word and Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length records that the classification of order-convex sets into the nine written forms is not proved here). No compactness and no boundedness is assumed: $I$ may be open, half-open, unbounded, or a single point.

Facts & Assumptions

Given: An order-convex $I \subseteq \mathbb{R}$ and a continuous injective $f : I \to \mathbb{R}$ .

[L1]

A continuous injective function on an order-convex subset of $\mathbb{R}$ is strictly monotone (A continuous injective function on an interval is strictly monotone).

[L2]

The image of an order-convex subset of the domain under a continuous function is order-convex (The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval, claim 1).

[L3]

If $J \subseteq \mathbb{R}$ is order-convex, $h : J \to \mathbb{R}$ satisfies $h(u) \le h(v)$ whenever $u, v \in J$ and $u \le v$ , and $h[J]$ is order-convex, then $h$ is continuous on $J$ (A function on an interval satisfying $f(x) \le f(y)$ whenever $x \le y$ , whose image is order-convex, is continuous).

[L4]

Sums, scalar multiples and composites of continuous functions are continuous; in particular $u \mapsto -u$ is continuous on every subset of $\mathbb{R}$ , being the scalar multiple $(-1)\,\mathrm{id}$ of the identity (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs).

[L5]

$f$ is injective, so $f : I \to f[I]$ is a bijection and has a unique two-sided inverse (Injection, surjection, bijection).

[L6]

$f$ increasing means $f(x) < f(y)$ whenever $x < y$ in $I$ ; $-f$ is decreasing exactly when $f$ is increasing, and $-S$ is order-convex exactly when $S$ is (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$ , with the dictionary to monotone sequences, Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1

Claim 1 is immediate: $f$ is continuous and injective on the order-convex set $I$ , hence strictly monotone.

1.2

Claim 2 is immediate: $I$ is order-convex and $f$ is continuous on $I$ , so $f[I]$ is order-convex.

1.3

Claim 3 is immediate: $f$ is injective and $f : I \to f[I]$ is onto its image by definition of the image, so it is a bijection and has a unique two-sided inverse $g : f[I] \to I$ .

2.1

Suppose $f$ is increasing, and let $u, v \in f[I]$ with $u < v$ . Write $u = f(p)$ and $v = f(q)$ with $p = g(u)$ and $q = g(v)$ in $I$ . If $q \le p$ then $f(q) \le f(p)$ , since $q = p$ gives equality and $q < p$ gives $f(q) < f(p)$ ; that is $v \le u$ , contradicting $u < v$ . Hence $p < q$ , that is $g(u) < g(v)$ , and $g$ is increasing.

step 1.1step 1.3L6

2.2

Suppose instead that $f$ is decreasing, and put $F := -f$ , that is $F(x) := -f(x)$ . Then $F$ is continuous on $I$ , it is injective because $f$ is, and it is increasing.

step 1.1L4L6

3.1

Still with $f$ increasing: $g$ satisfies $g(u) \le g(v)$ whenever $u \le v$ in $f[I]$ , by step 2.1 when $u < v$ and trivially when $u = v$ ; the domain $f[I]$ is order-convex by step 1.2; and the image $g[f[I]]$ is $I$ , which is order-convex, because $g$ is onto $I$ . So the monotone-with-interval-image criterion applies and $g$ is continuous on $f[I]$ .

step 1.2step 1.3step 2.1L3

4.1

By steps 2.1 and 3.1 applied to $F$ , the inverse $G : F[I] \to I$ of $F$ is increasing and continuous, and $F[I] = -f[I]$ is order-convex.

step 2.1step 3.1step 2.2

5.1

For $u \in f[I]$ one has $-u \in F[I]$ and $G(-u) = g(u)$ , since $F(g(u)) = -f(g(u)) = -u$ and $G$ is the inverse of $F$ . So $g$ is the composite of the continuous map $u \mapsto -u$ from $f[I]$ into $F[I]$ with the continuous $G$ , hence continuous on $f[I]$ .

step 1.3step 4.1L4

6.1

In that case $g$ is decreasing: for $u < v$ in $f[I]$ one has $-v < -u$ in $F[I]$ , so $G(-v) < G(-u)$ because $G$ is increasing, that is $g(v) < g(u)$ .

step 4.1step 5.1

7.1

Claims 4 and 5 are now proved in both cases: for $f$ increasing by steps 2.1 and 3.1, and for $f$ decreasing by steps 5.1 and 6.1; and by step 1.1 there is no other case.

step 1.1step 2.1step 3.1step 5.1step 6.1∎

Remarks

No epsilon-delta argument appears anywhere. Continuity of the inverse is obtained entirely from A function on an interval satisfying $f(x) \le f(y)$ whenever $x \le y$ , whose image is order-convex, is continuous, whose hypotheses are exactly the two facts the theorem has already established: the inverse is monotone, and its image is the order-convex set $I$ . The decreasing case is reduced to the increasing one by composing with $u \mapsto -u$ rather than repeating the argument.
What the theorem is used for. It is the tool that turns a strictly monotone continuous bijection into a continuous one in the other direction, and the standard elementary functions are built with it: the companion page derives the continuity of $x \mapsto x^{1/n}$ this way.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 96 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Inverse function theorem (Wikipedia) (standard reference, not scraped)
Monotonic function (Wikipedia) (standard reference, not scraped)
Real Analysis Notes 10 (California State University, Dominguez Hills) (standard reference, not scraped)

Continuous inverse theorem: a continuous injective fff on an interval III is a bijection onto the order-convex set f[I]f[I]f[I], and the inverse g:f[I]→Ig : f[I] \to Ig:f[I]→I is continuous and strictly monotone in the same sense as fff