Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Norm closed convex iff weakly closed

Statement

Assume HB (The real dominated-extension principle as an additional hypothesis over ZF). In a real or complex normed space, a convex set is norm closed if and only if it is weakly closed. More generally, its norm and weak closures coincide. Convexity here uses real coefficients.

Facts & Assumptions

[F1]

The weak topology is the initial topology of bounded scalar-linear functionals and is contained in the norm topology (Weak topology on a normed space).

[F2]

Under HB, a point outside a nonempty norm-closed convex set is uniformly strictly separated by the real part of a bounded scalar-linear functional (Relative geometric Hahn–Banach with the exact open, closed, and compact hypotheses).

Proof

Given: HB and a convex subset C of a real or complex normed space X.

1.1givenF1

Since weak-open sets are norm open, weak-closed sets are norm closed, and C‾∥⋅∥⊆C‾w. If C=∅, both closures are empty.

2.1step 1.1F2algebra

For nonempty C, put K=C‾∥⋅∥. It is convex: for u,v∈K and 0<t<1, approximate u,v by points a,b∈C within any positive δ; then ta+(1−t)b∈C and its distance from tu+(1−t)v is less than δ. The cases t=0,1 are just v,u∈K. Thus K is nonempty, closed and convex. For each x∉K, separation gives f∈X∗ and a real level a with Re⁡f(z)<a<Re⁡f(x) for all z∈K.

3.1step 2.1step 1.1F1

The set {y:Re⁡f(y)>a} is weakly open, contains x and misses C. Therefore x∉C‾w, giving C‾w⊆K and equality of closures. If C is norm closed this equality makes it weakly closed; the reverse implication was step 1.1. □

Depends on

Used by

Dependency tree · two levels

13 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