Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)(-\pi/2,\pi/2) onto R\mathbb R

Statement

The restriction

tan⁡:(−π/2,π/2)⟶R\tan:(-\pi/2,\pi/2)\longrightarrow\mathbb 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⁡2x(\tan x)'=\sec^2x; 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 cc is continuous at cc).

[L2]

On the natural domain of tangent, sec⁡2x=1+tan⁡2x\sec^2x=1+\tan^2x; moreover sec⁡x=1/cos⁡x≠0\sec x=1/\cos x\ne0, so sec⁡2x>0\sec^2x>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↦(cos⁡t,sin⁡t)t\mapsto(\cos t,\sin t) maps [0,2π)[0,2\pi) bijectively onto the unit circle (t↦(cos⁡t,sin⁡t)t\mapsto(\cos t,\sin t) is a bijection from [0,2π)[0,2\pi) onto the real unit circle).

[L4]

Cosine decreases on [0,π][0,\pi], increases on [π,2π][\pi,2\pi], has zeros at π/2\pi/2 and 3π/23\pi/2 in [0,2π)[0,2\pi), and sine and cosine have period 2π2\pi (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 a≥0\sqrt{a} \ge 0 with (a)2=a(\sqrt{a})^2 = a; the positives are {x2:x≠0}\{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 II, for ff continuous on II and differentiable at every interior point: f′≥0f' \ge 0 throughout gives ff nondecreasing, f′>0f' > 0 gives ff increasing, f′≤0f' \le 0 and f′<0f' < 0 give the two decreasing forms; conversely a nondecreasing ff has f′≥0f' \ge 0 and a nonincreasing ff has f′≤0f' \le 0 wherever it is differentiable, and no strict converse is claimed).

Proof

technique · direct
1.1

By [L4], cosine is positive on (−π/2,π/2)(-\pi/2,\pi/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.

L1L2L4L6
1.2

Fix y∈Ry\in\mathbb R and put c:=11+y2,s:=y1+y2.c:=\frac1{\sqrt{1+y^2}},\qquad s:=\frac y{\sqrt{1+y^2}}. The radicand is positive, c>0c>0, and c2+s2=1c^2+s^2=1. Thus [L3] supplies a unique t∈[0,2π)t\in[0,2\pi) with (cos⁡t,sin⁡t)=(c,s)(\cos t,\sin t)=(c,s).

L3L5algebra
2.1

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

step 1.2L1L4
3.1

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

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 28 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