Alphabeta MathHow 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.
The unit circle is locally a graph at every point
Example
At every point of the unit circle , the circle is locally the graph of a function of one coordinate.
Facts & Assumptions
Given: No hypotheses beyond those quantified in the statement.
On an open domain, a map satisfying can be solved locally for the second block when is invertible (The Euclidean implicit function theorem with derivative formula).
Direct difference quotients give and ; their displayed affine formulas are continuous. Thus the continuous-partials theorem gives , and is (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, Continuously differentiable maps, local inverses, and local diffeomorphisms, For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).
Proof
Let . Then [L2] gives . At a point on the circle, at least one of is nonzero.
If , then is multiplication by and is invertible, so [L1] expresses the circle locally as . If , exchange the coordinate blocks and obtain . These alternatives cover every circle point by step 1.1.
Depends on
- The Euclidean implicit function theorem with derivative formula
- Continuously differentiable maps, local inverses, and local diffeomorphisms
- If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative
- Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 101 results over 26 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
- J. Lebl, Basic Analysis II, §8.5.1 and Exercise 8.5.1 (standard reference, not scraped)