TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedaudited 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.

Separate a point from an open convex set

Statement

Assume the Axiom of Choice. Let $U$ be a nonempty open convex subset of a real or complex normed space $X$ and let $x_{0} \notin U$ . Then a nonzero $f \in X^{*}$ satisfies

$Re f (u) < Re f (x_{0}) (u \in U) .$

Facts & Assumptions

Given: The Axiom of Choice, a nonempty open convex $U$ and $x_{0} \notin U$ .

[F1]

If an open convex set contains $0$ , it equals the strict unit sublevel set of its gauge (An open convex neighbourhood is recovered from its gauge).

[F2]

Assuming the Axiom of Choice, a real linear functional dominated by a sublinear functional on a linear subspace extends to the whole real vector space with the same domination (Hahn-Banach dominated extension theorem for real vector spaces).

[F3]

A real linear functional $u$ on a complex space yields the complex-linear functional $u (x) - i u (i x)$ with real part $u$ (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).

[F4]

The gauge of a convex absorbing set is a real sublinear functional (The gauge of a convex absorbing set is sublinear).

Proof

technique · direct

1.1

Choose $u_{0} \in U$ and put $V = U - u_{0}$ , $y = x_{0} - u_{0}$ . Then $y \neq 0$ and $V$ is open, convex, contains $0$ , and $y \notin V$ ; by [F1], $p_{V} (y) \geq 1$ and $p_{V} (v) < 1$ for $v \in V$ .

givenF1choose

2.1

By [F1], $V$ is absorbing, and [F4] makes $p_{V}$ sublinear. On the real line $R y$ define $g (t y) = t$ . For $t \geq 0$ , $g (t y) = t \leq t p_{V} (y) = p_{V} (t y)$ ; for $t < 0$ , $g (t y) < 0 \leq p_{V} (t y)$ . Thus [F2] gives a real linear $h$ on $X$ with $h \leq p_{V}$ and $h (y) = 1$ .

step 1.1F1F2F4construct

3.1

Choose $r > 0$ with $B (0, r) \subseteq V$ . For $t > ∥ z ∥ / r$ one has $z / t \in V$ and $- z / t \in V$ , so taking infima gives $p_{V} (\pm z) \leq ∥ z ∥ / r$ . Domination applied to both $z$ and $- z$ gives $∣ h (z) ∣ \leq ∥ z ∥ / r$ . In the real case take $f = h$ ; in the complex case take $f (z) = h (z) - i h (i z)$ , which is continuous by this estimate and has real part $h$ by [F3].

step 2.1F3given

4.1

For $u = u_{0} + v \in U$ , [F1] and $h \leq p_{V}$ give $Re f (u) - Re f (u_{0}) = h (v) < 1 = h (y) = Re f (x_{0}) - Re f (u_{0})$ . Since $h (y) = 1$ , $f$ is nonzero. Hence the stated strict separation holds.

step 1.1step 2.1step 3.1F1algebra∎

Depends on

Used by

Separation of disjoint convex sets when one is open Theorem

Dependency tree · two levels

14 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, Theorems 5.2--5.3 (standard reference, not scraped)