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.

The composite of holomorphic maps is holomorphic and its complex Jacobian is the product

Statement

Let $m, n, p \geq 1$ , let $U \subseteq C^{m}$ and $V \subseteq C^{n}$ be open, let $F : U \to C^{n}$ have $F (U) \subseteq V$ and be holomorphic at $a \in U$ , and let $G : V \to C^{p}$ be holomorphic at $F (a)$ . Then $G \circ F$ is holomorphic at $a$ with

$D (G \circ F) (a) = D G (F (a)) \circ D F (a), J_{C} (G \circ F) (a) = J_{C} G (F (a)) J_{C} F (a) .$

Facts & Assumptions

Given: Open sets $U \subseteq C^{m}$ and $V \subseteq C^{n}$ , a map $F : U \to V$ holomorphic at $a$ , and $G : V \to C^{p}$ holomorphic at $F (a)$ ; the spaces are read through Complex $m$ -space and its real coordinate dictionary.

[L1]

$F$ is holomorphic 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$ ; $L$ is unique, written $D F (a)$ , and $J_{C} F (a)$ is its matrix in the standard bases (Holomorphic maps $C^{m} \to C^{n}$ and the complex Jacobian matrix, Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases, Finite rectangular matrices over a commutative ring, their entries, rows and columns).

[L2]

A map into $C^{n}$ is holomorphic exactly when each component is, with $D F (a) h$ the tuple of the component differentials (A map into $C^{n}$ is holomorphic exactly when each of its components is).

[L3]

A holomorphic function of several variables is continuous (A holomorphic function of several variables is continuous and separately holomorphic).

[L4]

$[S \circ T]_{B}^{D} = [S]_{C}^{D} [T]_{B}^{C}$ for linear $T : U^{'} \to V^{'}$ and $S : V^{'} \to W^{'}$ with ordered bases $B, C, D$ ( $[S \circ T]_{B}^{D} = [S]_{C}^{D} [T]_{B}^{C}$ ).

[L5]

For every linear $L : R^{m^{'}} \to R^{n^{'}}$ there is $K \geq 0$ with $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ), the notion of linear map being that of A linear map $L : R^{m} \to R^{n}$ in Euclidean coordinates.

[L6]

If $f$ is totally differentiable at $a$ and $g$ at $f (a)$ , then $g \circ f$ is totally differentiable at $a$ with $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L7]

Every $h$ 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$ ).

[L8]

$∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ for complex $z, w$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L9]

A set is open exactly when each of its points admits a ball inside it (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

Proof

technique · direct

1.1

Write $F (a + h) = F (a) + D F (a) h + r_{F} (h)$ and, for $κ \in C^{n}$ small, $G (F (a) + κ) = G (F (a)) + D G (F (a)) κ + r_{G} (κ)$ as in [L1], with $∥ r_{F} (h) ∥ = o (∥ h ∥)$ , $∥ r_{G} (κ) ∥ = o (∥ κ ∥)$ and $r_{G} (0) = 0$ . By [L5], read through the dictionary, there are $K, K^{'} \geq 0$ with $∥ D F (a) h ∥ \leq K ∥ h ∥$ and $∥ D G (F (a)) κ ∥ \leq K^{'} ∥ κ ∥$ .

givenL1L5

2.1

Put $κ (h) = D F (a) h + r_{F} (h)$ , so $F (a + h) = F (a) + κ (h)$ ; by step 1.1 and [L8] there is $δ > 0$ with $∥ κ (h) ∥ \leq (K + 1) ∥ h ∥$ whenever $∥ h ∥ < δ$ and $a + h \in U$ , and $F (a + h) \in V$ because $F (U) \subseteq V$ .

step 1.1L8L9

3.1

Substituting, $G (F (a + h)) = G (F (a)) + D G (F (a)) D F (a) h + ϱ (h)$ with $ϱ (h) = D G (F (a)) r_{F} (h) + r_{G} (κ (h))$ . By step 1.1 the first summand has norm at most $K^{'} ∥ r_{F} (h) ∥ = o (∥ h ∥)$ ; by step 2.1 the second has norm $o (∥ κ (h) ∥)$ with $∥ κ (h) ∥ \leq (K + 1) ∥ h ∥$ , hence $o (∥ h ∥)$ , the value at $h$ with $κ (h) = 0$ being $0$ . So $∥ ϱ (h) ∥ = o (∥ h ∥)$ by [L8].

step 1.1step 2.1L8

4.1

The composite $D G (F (a)) \circ D F (a)$ is $C$ -linear, being a composite of $C$ -linear maps, so step 3.1 and [L1] make $G \circ F$ holomorphic at $a$ with $D (G \circ F) (a) = D G (F (a)) \circ D F (a)$ ; this agrees with the real chain rule of [L6] read through the dictionary, by the uniqueness in [L1].

step 3.1L1L6

5.1

Taking matrices in the standard bases, [L4] turns step 4.1 into $J_{C} (G \circ F) (a) = J_{C} G (F (a)) J_{C} F (a)$ , the entries being read off at the basis vectors by [L2], [L3] and [L7].

step 4.1L1L2L3L4L7∎

Depends on

Used by

Dependency tree · two levels

71 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.3 (standard reference, not scraped)