PropositionStatement: AI-adaptedProof: 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 of several variables is continuous and separately holomorphic

Statement

Let $U \subseteq C^{m}$ be open and let $f : U \to C$ be holomorphic (Holomorphic functions on an open subset of $C^{m}$ ). Then $f$ is continuous on $U$ and separately holomorphic on $U$ (Separately holomorphic functions). Moreover, for $a \in U$ and $k < m$ the slice $f_{a, k}$ is complex differentiable at $a_{k}$ with derivative $D f (a) e_{k}$ , and

$D f (a) e_{k} = \partial_{z_{k}} f (a), D f (a) h = \sum_{k < m} (\partial_{z_{k}} f (a)) h_{k} .$

Facts & Assumptions

Given: An open $U \subseteq C^{m}$ and a holomorphic $f : U \to C$ ; $C^{m}$ is read through Complex $m$ -space and its real coordinate dictionary.

[L1]

$f$ is complex differentiable at $a$ when there is a $C$ -linear $L$ with $f (a + h) = f (a) + L (h) + r (h)$ and $∣ r (h) ∣ / ∥ h ∥ \to 0$ ; that $L$ is unique and written $D f (a)$ (Holomorphic functions on an open subset of $C^{m}$ ).

[L2]

$f$ is separately holomorphic when every slice $f_{a, k}$ is holomorphic on the open set $U_{a, k}$ in the one-variable sense (Separately holomorphic functions, Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[L3]

An $R$ -linear $T : C^{m} \to C$ has a unique representation $T (h) = \sum_{k < m} c_{k} h_{k} + \sum_{k < m} d_{k} \overline{h_{k}}$ , and $T$ is $C$ -linear exactly when every $d_{k} = 0$ ; for $T = D f (a)$ at a point of real total differentiability, $c_{k} = \partial_{z_{k}} f (a)$ and $d_{k} = \partial_{{\overset{ˉ}{z}}_{k}} f (a)$ (A real-linear functional on $C^{m}$ is complex linear exactly when its antiholomorphic part vanishes, Wirtinger operators in $C^{m}$ ).

[L4]

For every linear $L : R^{m} \to R^{n}$ there is $K \geq 0$ with $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for every $h$ (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ).

[L5]

A complex differentiable function of one variable is continuous (Complex differentiability at a point implies continuity there).

[L6]

Every $h \in C^{m}$ satisfies $h = \sum_{k < m} h_{k} e_{k}$ in the standard basis (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[L7]

$∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive); finite sums are additive, scale and are monotone in their terms (Laws of finite sums and finite products).

[L8]

Continuity of a map into $R^{n}$ from a subset of a metric space is the usual $ε$ – $δ$ condition with the Euclidean norm (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

Proof

technique · direct

1.1

Fix $a \in U$ and write $L = D f (a)$ as in [L1]. Since $L$ is $C$ -linear it is in particular $R$ -linear, so [L4] read through the dictionary gives $K \geq 0$ with $∣ L (h) ∣ \leq K ∥ h ∥$ for every $h$ ; alternatively [L3] and [L6] give $L (h) = \sum_{k < m} c_{k} h_{k}$ with $∣ c_{k} ∣ = ∣ L (e_{k}) ∣$ , and [L7] bounds $∣ L (h) ∣$ by $(\sum_{k < m} ∣ c_{k} ∣) ∥ h ∥$ because $∣ h_{k} ∣ \leq ∥ h ∥$ .

givenL1L3L4L6L7

1.2

The remainder satisfies $∣ r (h) ∣ / ∥ h ∥ \to 0$ by [L1], so there is $δ > 0$ with $∣ r (h) ∣ \leq ∥ h ∥$ whenever $0 < ∥ h ∥ < δ$ and $a + h \in U$ .

givenL1

1.3

Fix $k < m$ , let $a \in U$ and let $ζ \in U_{a, k}$ . The point $a^{'}$ obtained from $a$ by replacing its $k$ th coordinate by $ζ$ lies in $U$ and agrees with $a$ off the $k$ th coordinate, so $U_{a^{'}, k} = U_{a, k}$ and $f_{a^{'}, k} = f_{a, k}$ .

givenL2

2.1

Combining steps 1.1 and 1.2, $∣ f (a + h) - f (a) ∣ \leq ∣ L (h) ∣ + ∣ r (h) ∣ \leq (K + 1) ∥ h ∥$ for such $h$ , which tends to $0$ with $∥ h ∥$ ; by [L8] this is continuity of $f$ at $a$ , and $a \in U$ was arbitrary.

step 1.1step 1.2L7L8

2.2

With $a^{'}$ as in step 1.3 and $h = (ξ - ζ) e_{k}$ for $ξ$ near $ζ$ , [L1] and [L6] give $f_{a, k} (ξ) - f_{a, k} (ζ) = D f (a^{'}) e_{k} (ξ - ζ) + r (h)$ , and $∥ h ∥ = ∣ ξ - ζ ∣$ by the dictionary, so $∣ r (h) ∣ / ∣ ξ - ζ ∣ \to 0$ . Hence $f_{a, k}$ is complex differentiable at $ζ$ with derivative $D f (a^{'}) e_{k}$ ; as $ζ \in U_{a, k}$ was arbitrary, the slice is holomorphic on $U_{a, k}$ and $f$ is separately holomorphic by [L2].

step 1.3L1L2L6

3.1

By [L3] applied to the $C$ -linear $D f (a)$ , every $d_{k}$ vanishes and $D f (a) h = \sum_{k < m} c_{k} h_{k}$ with $c_{k} = D f (a) e_{k} = \partial_{z_{k}} f (a)$ ; step 2.2 at $ζ = a_{k}$ identifies that number with the derivative of the slice, and [L5] confirms the slice is continuous, consistently with step 2.1.

step 2.1step 2.2L3L5L6∎

Depends on

Used by

Dependency tree · two levels

79 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, §1.2 (standard reference, not scraped)