TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31

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.

Two real-analytic functions on an open interval that agree on a set with an accumulation point in that interval agree throughout the interval

Statement

Let $I \subseteq R$ be an open interval and let $f, g : I \to R$ be real analytic. If the agreement set ${x \in I : f (x) = g (x)}$ has an accumulation point $c$ lying inside $I$ , then $f = g$ throughout $I$ .

Facts & Assumptions

Given: The interval, functions, agreement set, and interior accumulation point in the statement.

[L1]

Subtracting local power-series representations shows directly that $h : = f - g$ is real analytic (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series).

[L2]

At a zero of a real-analytic function, the zero is isolated unless the function vanishes on a neighbourhood (At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes).

[L3]

Every interval is connected: it has no decomposition into two nonempty separated sets, where each set must avoid the closure of the other (A subset of $R$ is connected if and only if it is order-convex, that is, an interval, Separated sets, disconnection, and connected subset of $R$ ).

[L4]

Local power-series sums are continuous (The sum of a real power series is continuous at every point strictly inside its interval of convergence).

Proof

technique · direct

1.1

Put $h : = f - g$ . By [L1], $h$ is real analytic. The accumulating zeros and [L4] give $h (c) = 0$ , and this zero is not isolated; hence [L2] makes $h$ identically zero on a neighbourhood of $c$ .

givenL1L2L4

2.1

Let $V$ be the set of points of $I$ having a neighbourhood in $I$ on which $h$ vanishes. Step 1.1 makes $V$ nonempty, and its definition makes it relatively open.

step 1.1

3.1

The complement $I ∖ V$ is also relatively open. Indeed, if $h (x) \neq 0$ , continuity gives a neighbourhood containing no zero and hence no point of $V$ ; if $h (x) = 0$ but $x \notin V$ , [L2] makes $x$ an isolated zero, and a sufficiently small neighbourhood again contains no point of $V$ .

step 2.1L2L4

4.1

Steps 2.1 and 3.1 make $V$ and $I ∖ V$ separated: every point of either set has a real neighbourhood disjoint from the other, so neither set meets the closure of the other. If $I ∖ V$ were nonempty, they would therefore disconnect the connected interval $I$ , contrary to [L3]. Thus $V = I$ and $h = 0$ throughout $I$ , so $f = g$ .

step 2.1step 3.1L3∎

Depends on

Used by

The area theorem for exterior univalent functions Theorem

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Analytic function, Encyclopedia of Mathematics (standard reference, not scraped)
Power series, Encyclopedia of Mathematics (standard reference, not scraped)
Northwestern Math 320-2 lecture notes (standard reference, not scraped)