TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically

Statement

Let $m \geq 1$ , let $U \subseteq C^{m}$ be a nonempty connected open set, and let $f : U \to C$ be holomorphic (Holomorphic functions on an open subset of $C^{m}$ ). If there is a nonempty open set $W \subseteq U$ such that $f (z) = 0$ for every $z \in W$ , then $f \equiv 0$ on $U$ .

This is the several-variable identity theorem at the strength the page supports: the hypothesis is a nonempty open set of zeros. An accumulation point of the zero set is neither assumed nor sufficient in several variables; the companion page records that stronger one-variable statement as false here.

Facts & Assumptions

Given: A nonempty connected open set $U \subseteq C^{m}$ , a holomorphic function $f : U \to C$ , and a nonempty open set $W \subseteq U$ on which $f = 0$ .

[L1]

Holomorphic functions of several variables are smooth; every point $a \in U$ has a polydisc $Δ_{r} (a) \subseteq U$ on which $f (z) = \sum_{α} c_{α} (z - a)^{α}, c_{α} = \frac{\partial_{z}^{α} f (a)}{α!};$ and all mixed complex derivatives are holomorphic (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).

[L2]

A connected space has no nontrivial clopen subsets (For a topological space the following agree: no separation exists, the only clopen subsets are $\emptyset$ and $X$ , and every continuous map to the two-point discrete space is constant, Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[L3]

The mixed complex derivative notation $\partial_{z}^{α}$ and the zero-order identity $\partial_{z}^{0} f = f$ are those in the power-series and smoothness statement [L1]; $C^{k}$ maps and multi-index derivative notation in Euclidean space supplies the underlying multi-index arithmetic.

[L4]

Polydiscs in $C^{m}$ are the coordinatewise discs of Balls, polydiscs and the distinguished boundary in $C^{m}$ .

Proof

technique · direct

1.1

For every multi-index $α$ , the derivative $\partial_{z}^{α} f$ is holomorphic and therefore continuous on $U$ by [L1]; since $f = 0$ on the open set $W$ , every derivative of $f$ is also $0$ on $W$ , so the set $A : = {z \in U : \partial_{z}^{α} f (z) = 0 for every α}$ contains $W$ and is therefore nonempty.

givenL1L3

2.1

The set $A$ is closed in $U$ , because it is the intersection over all multi-indices $α$ of the closed zero sets of the continuous functions $\partial_{z}^{α} f$ .

step 1.1

2.2

The set $A$ is open in $U$ : if $a \in A$ , choose a smaller polydisc $Δ \subseteq U$ centred at $a$ ; then every coefficient $\partial^{α} f (a) / α!$ in the power-series expansion of $f$ on $Δ$ is $0$ , so [L1] gives $f = 0$ on $Δ$ , and hence every derivative vanishes on $Δ$ as well, which means $Δ \subseteq A$ .

step 1.1L1L4

3.1

The set $A$ is a nonempty subset of $U$ that is both open in $U$ and closed in $U$ , so connectedness and [L2] force $A = U$ ; in particular $f = \partial_{z}^{0} f$ vanishes at every point of $U$ , hence $f \equiv 0$ on $U$ .

step 2.1step 2.2L2L3∎

Remarks

Why the hypothesis is open-set vanishing and not an accumulation point. In one complex variable, accumulation of zeros implies equality by local factorisation and isolated zeros. In several variables the zero set of a nonzero holomorphic function can contain whole complex hypersurfaces, so the open-set hypothesis is the honest form at this stage.
What the proof really uses. The proof needs only two page-level tools: holomorphic smoothness and the local power-series expansion. Once every derivative at one point vanishes, the power series on a smaller polydisc is identically zero, and connectedness propagates that local vanishing to the whole set.

Depends on

Used by

Dependency tree · two levels

42 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

J. Lebl, Tasty Bits of Several Complex Variables, v4.4, Thm. 1.2.7 (standard reference, not scraped)
H. P. Boas, Lecture Notes on Multidimensional Complex Analysis, Ch. 2 (standard reference, not scraped)
M. Jabbari, Notes for Analysis and Geometry of Several Complex Variables, Thm. 22(7) (standard reference, not scraped)