TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Oka-Weil approximation on a pseudoconvex domain

Statement

Assume the Axiom of Choice (AC). Let $Ω \subseteq C^{n}$ be a domain that is Hartogs pseudoconvex (Plurisubharmonic exhaustions and Hartogs pseudoconvexity), let $K ⋐ Ω$ be compact with ${\hat{K}}_{Ω} = K$ (Holomorphic hulls and holomorphic convexity), and let $f$ be holomorphic in an open neighbourhood of $K$ . Then for every $ε > 0$ there is $F \in O (Ω)$ with $\sup_{z \in K} ∣ F (z) - f (z) ∣ < ε .$

Facts & Assumptions

Given: The Axiom of Choice; a Hartogs pseudoconvex domain $Ω \subseteq C^{n}$ ; a compact $K ⋐ Ω$ with ${\hat{K}}_{Ω} = K$ ; a holomorphic $f$ on an open neighbourhood of $K$ ; a real number $ε > 0$ .

[F1]

For a domain $Ω \subseteq C^{n}$ the following three conditions are equivalent: $Ω$ is Hartogs pseudoconvex; $Ω$ is a domain of holomorphy; $Ω$ is holomorphically convex (The Levi problem: pseudoconvexity, domains of holomorphy, and holomorphic convexity).

[F2]

If $G$ is a domain of holomorphy, $A ⋐ G$ is compact with ${\hat{A}}_{G} = A$ , and $g$ is holomorphic in an open neighbourhood of $A$ , then for every $δ > 0$ there is $H \in O (G)$ with $\sup_{A} ∣ H - g ∣ < δ$ (Oka-Weil approximation on a domain of holomorphy (host-domain lemma)).

[F3]

AC is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice).

Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F3]; it is consumed only inside the suppliers [F1] and [F2], each of which carries its own choice hypotheses. The proof selects nothing.

Proof

technique · direct

1.1F1given

By [F1] the Hartogs pseudoconvex domain $Ω$ is a domain of holomorphy.

2.1F2F3step 1.1given∎

Applying [F2] with $G : = Ω$ , $A : = K$ , ${\hat{A}}_{G} = A$ and $g : = f$ , and with $δ : = ε$ , gives $F \in O (Ω)$ with $\sup_{K} ∣ F - f ∣ < ε$ , which is the assertion of the Statement under the ambient Axiom of Choice cited as [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

Harold P. Boas, Lecture Notes on Several Complex Variables (standard reference, not scraped)
Jiri Lebl, Tasty Bits of Several Complex Variables (standard reference, not scraped)