LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03

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.

Tangent is a continuous strictly increasing bijection from $(- π / 2, π / 2)$ onto $R$

Statement

The restriction

$\tan : (- π / 2, π / 2) ⟶ R$

is continuous, strictly increasing, and bijective.

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Tangent is defined where cosine is nonzero and is differentiable on its natural domain with $(\tan x)^{'} = \sec^{2} x$ ; differentiability there implies continuity (Tangent, cotangent, secant, and cosecant on their exact natural domains, Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant, A function differentiable at $c$ is continuous at $c$ ).

[L2]

On the natural domain of tangent, $\sec^{2} x = 1 + \tan^{2} x$ ; moreover $\sec x = 1 / \cos x \neq 0$ , so $\sec^{2} x > 0$ (Pythagorean and parity identities for all six trigonometric functions on their natural domains, Tangent, cotangent, secant, and cosecant on their exact natural domains, Squares of nonzero elements are positive).

[L3]

The map $t \mapsto (\cos t, \sin t)$ maps $[0, 2 π)$ bijectively onto the unit circle ( $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle).

[L4]

Cosine decreases on $[0, π]$ , increases on $[π, 2 π]$ , has zeros at $π / 2$ and $3 π / 2$ in $[0, 2 π)$ , and sine and cosine have period $2 π$ (Signs, monotonicity intervals, and ranges of sine and cosine, The zero sets of sine and cosine and the least positive common period 2 pi).

[L5]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L6]

A continuous function on an interval whose derivative is positive at every interior point is strictly increasing (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed).

Proof

technique · direct

1.1L1L2L4L6

By [L4], cosine is positive on $(- π / 2, π / 2)$ , so tangent is defined and continuous there. By [L1], [L2], and [L6], its derivative is positive and the restriction is strictly increasing, hence injective.

1.2L3L5algebra

Fix $y \in R$ and put $c : = \frac{1}{\sqrt{1 + y^{2}}}, s : = \frac{y}{\sqrt{1 + y^{2}}} .$ The radicand is positive, $c > 0$ , and $c^{2} + s^{2} = 1$ . Thus [L3] supplies a unique $t \in [0, 2 π)$ with $(\cos t, \sin t) = (c, s)$ .

2.1step 1.2L1L4

Since $\cos t = c > 0$ , [L4] places $t$ in $[0, π / 2) \cup (3 π / 2, 2 π)$ . Set $u : = t$ in the first case and $u : = t - 2 π$ in the second. Then $u \in (- π / 2, π / 2)$ and periodicity of sine and cosine gives $\tan u = s / c = y$ . Hence the restriction is surjective.

3.1step 1.1step 2.1∎

Step 1.1 gives continuity and injectivity, while step 2.1 gives surjectivity.

Depends on

Dependency tree · 2 levels

Sources

NIST Digital Library of Mathematical Functions, §4.23 Inverse Trigonometric Functions