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.
Geometric Hahn Banach and Convex Separation Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Geometric Hahn Banach and Convex Separation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The Analytic Hahn Banach Theorem
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Logarithm and General Powers
- The Riemann Integral: Definition and Integrability
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
These examples compute gauges, show why balancedness and compactness hypotheses matter, and give both a dual distance formula and the classical closed, uncomplemented inclusion .
3 · Logical flowchart
4 · Definitions, theorems and proofs
The sequence spaces c_0 and ell-infinity
Definition
Let or , with absolute value in the real case and modulus in the complex case. A scalar sequence here is a function , including index zero. Let
both equipped with . Thus is a specified linear subspace of the bounded-sequence space .
Here means that for every real there is such that for all . Addition and scalar multiplication are coordinatewise. The scalar triangle inequality makes bounded sequences and null sequences linear spaces and gives the triangle inequality for the displayed supremum norm. Absolute homogeneity follows coordinatewise, and a zero supremum forces every coordinate to vanish.
c_0 is a closed subspace of ell-infinity
Statement
is a closed linear subspace of in the sup norm.
Facts & Assumptions
Given: The sequence spaces .
consists of bounded sequences tending to zero, with the sup norm (The sequence spaces c_0 and ell-infinity).
Proof
Sums and scalar multiples of null sequences are null, so is a linear subspace.
If and , choose with this norm below , then with for . Thus for .
Hence and the subspace is closed.
An uncountable almost-disjoint family of subsets of the naturals
Statement
There is an uncountable family of infinite subsets of such that is finite whenever are distinct.
Facts & Assumptions
Given: A fixed enumeration of and the set of irrational real numbers.
Every nonempty subset of has a least element (The well-ordering principle).
Every nonempty interval in contains a rational, and is uncountable (Both and are dense in , and every nonempty open subset of is uncountable, The irrationals are uncountable).
Proof
For , recursively let be the least unused index with , and put . Such an index exists by [F2] because every interval contains infinitely many rationals; [F1] makes the choice deterministic.
Each is infinite since its indices are chosen unused. If , then for sufficiently large the intervals and are disjoint; any common selected index must therefore arise among finitely many early choices. Thus is finite.
The map is injective by the finite-intersection conclusion, so is uncountable by [F2] and has the required property.
The quotient ell-infinity/c_0 has no countable separating family
Statement
Assume . The dual of has no countable family that separates its points.
Facts & Assumptions
Given: and an uncountable almost-disjoint family of infinite subsets of .
is closed in , so the quotient seminorm on is a norm (c_0 is a closed subspace of ell-infinity, The quotient seminorm is a norm exactly when the subspace is closed).
There is an uncountable almost-disjoint family of infinite subsets of (An uncountable almost-disjoint family of subsets of the naturals).
Assuming , a countable union of countable sets is countable (Countable unions of at most countable sets, assuming ).
Proof
For , let be its indicator sequence. Then in , and for distinct the quotient norm of is , since the supports are disjoint after deleting finitely many coordinates.
For and , the set is finite: choose scalar phases on any finite subfamily and apply . Thus is countable as a union over positive reciprocal integers.
Given a countable family in , [F3] makes countable. By [F2] choose outside it; then nonzero is annihilated by every .
c_0 is not complemented in ell-infinity
Statement
Assuming , the closed subspace is not complemented in .
Facts & Assumptions
Given: The quotient map .
Under , has no countable separating family (The quotient ell-infinity/c_0 has no countable separating family).
Proof
Suppose a bounded projection exists. For each coordinate , define . This is well defined because for , and it is a bounded functional on the quotient.
If for every , then coordinatewise, so and . Thus is a countable separating family.
This contradicts [F1]. Hence no such projection exists, and is not complemented.
Two results called Mazur's lemma
Remark
This page proves the result usually called Mazur's theorem: norm and weak closures of a convex set coincide (Mazur theorem: weak and norm closure agree for convex sets). Another result often called Mazur's lemma says that suitable convex combinations of a weakly convergent sequence converge in norm. That sequence-level result is not proved or used here.
5 · Examples, counterexamples and false statements
Gauges of norm balls and finite-dimensional ellipsoids
Example
For , . For a positive-definite real quadratic form on and , . Both are norms: the first is a positive scalar multiple of the given norm, and the second is the norm induced by the inner product associated with the positive-definite quadratic form .
Facts & Assumptions
Given: A radius and a positive-definite quadratic form .
The gauge of an absorbing set is the infimum of its admissible positive dilates (Minkowski functional of an absorbing set).
Verification
exactly when , whose infimum over is .
Likewise exactly when , so the infimum is . Positive definiteness gives zero only at , and the displayed formulas give norm homogeneity and triangle inequality.
A gauge of a nonbalanced set need not be a seminorm
Statement refuted
An absorbing convex set need not have a seminorm as its gauge.
Facts & Assumptions
Given: The convex absorbing set .
The gauge is the infimum of positive for which (Minkowski functional of an absorbing set).
Counterexample
From , [F1] gives for and for .
Hence while , contradicting the required equality . The missing hypothesis is balancedness.
Two closed convex sets can have no strong separator
Statement refuted
Two disjoint closed convex sets in a normed space always admit a strong separator.
Facts & Assumptions
Given: and in .
The exponential is continuous and convex (A function differentiable at is continuous at , The two-point convexity inequality for the exponential function).
Counterexample
is closed convex. By [F1], is the closed epigraph of a convex function, hence closed and convex; it is disjoint from because .
The points and have distance . A strong gap for would imply for all , impossible.
Distance to a subspace via annihilating functionals
Example
For a subspace and ,
Facts & Assumptions
Given: A subspace and .
A bounded linear functional on a subspace extends to the ambient normed space without changing its norm (A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed).
Verification
For with , continuity gives . Hence, for every , . Taking infima gives the direction.
Put . If , define by . This is well defined, and so . By [F1], extends to an with ; this extension lies in and satisfies . If , then , so continuity makes every annihilator vanish at . Thus equality holds in both cases.
A closed uncomplemented subspace
Example
Assuming , the inclusion is a concrete closed subspace that is not complemented.
Facts & Assumptions
Given: The standard inclusion .
is closed in (c_0 is a closed subspace of ell-infinity).
is not complemented in under (c_0 is not complemented in ell-infinity).
Verification
The inclusion in the statement is a closed-subspace inclusion by [F1].
It is uncomplemented by [F2], so it has both advertised properties.
Sources
- Piotr Hajlasz, Functional Analysis, §10.5
- Piotr Hajlasz, Functional Analysis, Lemma 10.20
- Piotr Hajlasz, Functional Analysis, proof of Theorem 10.19
- Piotr Hajlasz, Functional Analysis, Theorem 10.19
- Gerald Teschl, Topics in Real and Functional Analysis, Theorem 5.11
- Gerald Teschl, Topics in Real and Functional Analysis, §5.1 examples
- Gerald Teschl, Topics in Real and Functional Analysis, §5.1
- Gerald Teschl, Topics in Real and Functional Analysis, Problem 5.2
- Theo Buehler and Dietmar Salamon, Functional Analysis, Theorem 2.53