LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

A norm-closed convex set is weakly sequentially closed

Statement

Assume the Axiom of Choice. Let $X$ be a real or complex normed space and let $K \subseteq X$ be convex and closed in the norm topology. Then $K$ is closed in the weak topology $σ (X, X^{*})$ (Weak topology on a normed space); in particular $K$ is weakly sequentially closed: if $(u_{j}) \subseteq K$ and $u_{j} ⇀ u$ (Weak convergence of nets and sequences), then $u \in K$ .

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice); a real or complex normed space $X$ with dual $X^{*}$ ; a convex set $K \subseteq X$ that is closed in the norm topology. The weak topology is $σ (X, X^{*})$ (Weak topology on a normed space) and weak sequential convergence is as in Weak convergence of nets and sequences.

[F1]

Under the Axiom of Choice, two disjoint nonempty convex sets $C, K \subseteq X$ , with $C$ closed and $K$ compact, are strongly separated by a nonzero functional in $X^{*}$ (Strong separation of a closed and a compact convex set): there are $f \in X^{*}$ , $f \neq 0$ , and a positive gap $\sup_{C} Re f < \inf_{K} Re f$ .

[F2]

The weak topology is the initial topology of the maps $f : X \to K$ , $f \in X^{*}$ , hence every set ${y \in X : Re f (y) > α}$ with $f \in X^{*}$ and $α \in R$ is weakly open, and a subset of $X$ is weakly closed exactly when its complement is weakly open (Weak topology on a normed space).

[F3]

A sequence $u_{j} ⇀ u$ converges weakly in the sense of convergence in $σ (X, X^{*})$ ; a weakly closed set contains the limit of every weakly convergent sequence contained in it (Weak convergence of nets and sequences).

Proof

technique · direct, by separating an exterior point from $K$ with a weak half-space

1.1givenalgebra

Trivial case and set-up. If $K = \emptyset$ then $K$ is closed in every topology, so both assertions hold; assume henceforth $K \neq \emptyset$ and fix a point $x \in X ∖ K$ .

2.1F1step 1.1

Strong separation of $K$ and the singleton ${x}$ . The sets $K$ and ${x}$ are nonempty and convex, $K$ is closed in the norm topology and ${x}$ is compact; they are disjoint because $x \notin K$ . By [F1], applied here, there are $f \in X^{*}$ , $f \neq 0$ , and a real number $α$ with $\sup_{K} Re f \leq α < Re f (x)$ , the gap being the one supplied by the theorem.

3.1F2step 2.1

A weak neighbourhood of $x$ missing $K$ . Put $U : = {y \in X : Re f (y) > α}$ . By [F2] the set $U$ is open in $σ (X, X^{*})$ ; it contains $x$ because $Re f (x) > α$ , and it is disjoint from $K$ because every $y \in K$ satisfies $Re f (y) \leq \sup_{K} Re f \leq α$ .

4.1step 3.1F2

$K$ is weakly closed. Since $x \in X ∖ K$ was arbitrary and step 3.1 produces for it a weak neighbourhood $U \subseteq X ∖ K$ , the complement $X ∖ K$ is weakly open; equivalently $K$ is closed in the weak topology $σ (X, X^{*})$ .

5.1F3step 4.1∎

Weak sequential closedness. Let $(u_{j}) \subseteq K$ with $u_{j} ⇀ u$ . By [F3] the convergence is convergence in $σ (X, X^{*})$ , and a set closed in a topology contains the limit of every convergent sequence in it; hence $u \in K$ .

Depends on

Used by

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, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Francesco Paolo Maiale (course by Giovanni Alberti), Lecture Notes Calculus of Variations A, University of Pisa (last update 21 August 2019; complete 149-page notes) (standard reference, not scraped)