Alphabeta Math
CorollaryStatement: 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.

Weak closure of the unit sphere is the closed unit ball

Statement

Assume HB. In an infinite-dimensional real or complex normed space X, the weak closure of S={x:∥x∥=1} is B={x:∥x∥≤1}.

Facts & Assumptions

[F1]

A weak neighborhood contains finitely many coordinate disk conditions (Basic weak neighborhoods).

[F2]

Under HB, norm-closed convex sets are weakly closed (Norm closed convex iff weakly closed).

[F3]

A continuous real function on a closed bounded interval takes every value between its endpoint values, choice-free (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)).

Proof

Given: HB and infinite-dimensional X.

1.1givenF2algebra

The ball B is convex by the triangle inequality and norm closed because ∣∥x∥−∥y∥∣≤∥x−y∥. Thus B is weakly closed and contains S, giving S‾w⊆B.

2.1step 1.1F1givenalgebra

Fix x∈B and a weak neighborhood of x containing the conditions ∣fj(y−x)∣<ε, 1≤j≤m. There is a nonzero v with all fj(v)=0: choose m+1 independent vectors in X by finite induction; their images in Km are dependent, so a nonzero linear combination of the original vectors lies in the common kernel. This also covers m=0.

3.1step 2.1step 1.1F3algebra

If ∥x∥=1, the point x itself works. If ∥x∥<1, put T=(2+∥x∥)/∥v∥. The real function h(t)=∥x+tv∥ on [0,T] satisfies ∣h(t)−h(s)∣≤∣t−s∣∥v∥, h(0)<1, and h(T)≥T∥v∥−∥x∥=2>1. The intermediate value theorem gives t∈[0,T] with h(t)=1. Then y=x+tv∈S has fj(y−x)=0 for every j, so lies in the given neighborhood. Every neighborhood of every x∈B meets S, proving B⊆S‾w and equality. □

Depends on

Used by

Dependency tree · two levels

22 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