ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 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.

Componentwise holomorphy checked for an explicit map $C^{2} \to C^{3}$

Example

Define $F : C^{2} \to C^{3}$ by

$F (z_{0}, z_{1}) = (z_{0} z_{1}, z_{0} + z_{1}, \exp (z_{0})) .$

Then each component is holomorphic, so $F$ is holomorphic. Its complex Jacobian matrix is

$J_{C} F (z) = (\begin{array}{cc} z_{1} & z_{0} \\ 1 & 1 \\ \exp (z_{0}) & 0 \end{array}),$

and at the origin this becomes

$J_{C} F (0, 0) = (\begin{array}{cc} 0 & 0 \\ 1 & 1 \\ 1 & 0 \end{array}) .$

Facts & Assumptions

Given: The map $F (z_{0}, z_{1}) = (z_{0} z_{1}, z_{0} + z_{1}, \exp (z_{0}))$ .

[L1]

A map into $C^{n}$ is holomorphic exactly when each component is holomorphic (A map into $C^{n}$ is holomorphic exactly when each of its components is).

[L2]

Sums and products of holomorphic scalar functions are holomorphic (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).

[L3]

The complex exponential is entire and has derivative itself (The complex exponential is entire and its complex derivative is itself, The complex exponential by its power series).

[L4]

The complex Jacobian matrix records the derivatives $\partial F_{j} / \partial z_{k}$ (Holomorphic maps $C^{m} \to C^{n}$ and the complex Jacobian matrix).

Verification

technique · direct

1.1L2L3

The first component $(z_{0}, z_{1}) \mapsto z_{0} z_{1}$ and the second component $(z_{0}, z_{1}) \mapsto z_{0} + z_{1}$ are holomorphic by [L2], and the third component $(z_{0}, z_{1}) \mapsto \exp (z_{0})$ is holomorphic by [L3].

2.1step 1.1L1

Therefore [L1] makes $F$ holomorphic.

2.2step 1.1L3L4

By [L4], $\partial (z_{0} z_{1}) / \partial z_{0} = z_{1}$ , $\partial (z_{0} z_{1}) / \partial z_{1} = z_{0}$ , $\partial (z_{0} + z_{1}) / \partial z_{0} = \partial (z_{0} + z_{1}) / \partial z_{1} = 1$ , $\partial (\exp (z_{0})) / \partial z_{0} = \exp (z_{0})$ , and $\partial (\exp (z_{0})) / \partial z_{1} = 0$ , which gives the displayed matrix.

3.1step 2.2∎

Substituting $(z_{0}, z_{1}) = (0, 0)$ into that matrix gives the displayed value at the origin.

Depends on

Used by

The complex Jacobian and its determinant for (z₀z₁, z₀+z₁) Example

Dependency tree · two levels

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

Componentwise holomorphy checked for an explicit map C2→C3C2→C3