TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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.

Every boundary point belonging to a nonempty Euclidean convex set has a supporting hyperplane

Statement

Assume the Axiom of Choice (The Axiom of Choice) and the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n \geq 1$ , let $C \subseteq R^{n}$ be nonempty and convex, and let $a \in C \cap \partial C$ . Then there is a nonzero vector $u$ such that $⟨ u, z - a ⟩ \leq 0$ for every $z \in C$ . Thus the hyperplane through $a$ normal to $u$ supports $C$ (Supporting and strictly separating hyperplanes in Euclidean space).

Facts & Assumptions

Given: The countable-choice, boundary, and sequential-closure conventions in the Statement (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed) and compactness of the Euclidean unit sphere For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact.

[A1]

The Axiom of Choice supplies a choice function for every family of nonempty sets (The Axiom of Choice).

[A2]

The Axiom of Countable Choice supplies a choice function for every family of nonempty sets indexed by $N$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L0]

The closure $\overline{C}$ is convex, $int (C) = int (\overline{C})$ , and $\partial C = \partial \overline{C}$ (A convex set and its closure have the same interior and boundary).

[L1]

If $x$ lies outside a nonempty closed convex set, then there are $v \neq 0$ and $b \in R$ such that $⟨ v, z ⟩ \leq b < ⟨ v, x ⟩$ for every point $z$ of the set (A point outside a nonempty closed convex set is strictly separated from it).

[L2]

For $n \geq 1$ , every bounded sequence in $R^{n}$ has a convergent subsequence selected by a strictly increasing index map (For $n \geq 1$ every bounded sequence in $R^{n}$ has a convergent subsequence).

Proof

technique · direct

1.1

By [A1], [A2], and [L0], $a$ remains a boundary point after replacing $C$ by the closed convex set $\overline{C}$ . Since every ball about $a$ meets the complement, the sequence-producing direction of A point lies in the closure of $A$ iff some sequence in $A$ converges to it, and a set is closed iff it is sequentially closed uses [A2] to choose $x_{j} \notin \overline{C}$ with $x_{j} \to a$ . Apply [L1] to each $x_{j}$ and normalize its separating normal $u_{j}$ to length one; then $⟨ u_{j}, z - x_{j} ⟩ < 0 (z \in \overline{C}) .$

A1A2L0L1givenchoose

2.1

The unit normals are bounded, so [L2] gives a subsequence converging to a vector $u$ of norm one. For fixed $z \in \overline{C}$ , pass the inequalities of step 1.1 to the limit, using $x_{j} \to a$ , to obtain $⟨ u, z - a ⟩ \leq 0$ . The unit vector $u$ is nonzero, and the inequality holds in particular for $z \in C$ .

step 1.1L2algebra∎

Depends on

Used by

Dependency tree · two levels

57 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

S. Boyd and L. Vandenberghe, Convex Optimization, §2.5.2 (standard reference, not scraped)
D. Bertsekas, MIT 6.253 Convex Analysis and Optimization, Lecture 7 (standard reference, not scraped)