TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

Strong separation of a closed and a compact convex set

Statement

Let $C, K \subseteq X$ be disjoint nonempty convex sets, where $C$ is closed and $K$ is compact. Then they are strongly separated by a nonzero functional in $X^{*}$ .

Facts & Assumptions

Given: Disjoint nonempty convex $C, K$ , with $C$ closed and $K$ compact.

[F1]

Distance to a fixed nonempty set is continuous (indeed $1$ -Lipschitz) ( $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz).

[F2]

A continuous real-valued function on a compact metric space attains its minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F3]

Disjoint convex sets, one open, are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).

Proof

technique · direct

1.1

By [F1]--[F2], $d (k, C)$ has a minimum $δ$ on $K$ . It is positive: a zero minimum would put some $k \in K$ in the closed set $C$ . Choose $0 < r < δ$ .

F1F2givenchoose

2.1

The thickening $W = C + B (0, r)$ is open and convex and is disjoint from $K$ . Apply [F3] to $W, K$ to obtain nonzero $f$ with $Re f (w) < Re f (k)$ for $w \in W, k \in K$ .

step 1.1F3

3.1

For $c \in C$ , take the supremum over $b \in B (0, r)$ in the inequalities from step 2.1. Since $\sup_{∥ b ∥ < r} Re f (b) = r ∥ f ∥$ , this gives $Re f (c) + r ∥ f ∥ \leq Re f (k)$ for every $k \in K$ . Hence $\sup_{C} Re f + r ∥ f ∥ \leq \inf_{K} Re f$ , a positive gap.

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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

Gerald Teschl, Topics in Real and Functional Analysis, Corollary 5.4 (standard reference, not scraped)