TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\mathbb R$ be an open interval and let $f,g:I\to\mathbb 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 $\mathbb{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 $\mathbb{R}$ is connected if and only if it is order-convex, that is, an interval, Separated sets, disconnection, and connected subset of $\mathbb{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\setminus V$ is also relatively open. Indeed, if $h(x)\ne0$ , 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\setminus 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\setminus 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

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

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)