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.
Convex sets and continuous real-hyperplane separation in a normed space
Definition
Let be a normed space over using A norm on a real vector space, the induced metric, and the dictionary with the metric axioms over and Complex norm and complex normed space over , with metric supplied in the complex case by Realification preserves a complex norm and its metric. A subset is convex when where is real, also when . The empty set and every singleton are convex: the former has no pair of points to test, and for the latter. At the convex combination is one of its endpoints.
For a nonzero (the bounded scalar-linear dual of The dual space X^* of a normed space and its dual norm) put , with over . A continuous real affine hyperplane is a set for . For subsets , this hyperplane gives:
- weak separation if for all ;
- open-side strict separation in the indicated orientation if for all such ;
- uniform strict separation if there is with for all such .
Only real numbers are ordered in these formulas. The last condition requires one positive margin that works for all pairs, rather than merely pointwise strict inequalities.
Here is a nonzero bounded real-linear functional. Indeed, if in the complex case, put . Then ; over the real field, . Normalizing a nonzero vector in the dual-norm definition gives , also true at zero. Hence and . If , every with still has . Thus the complement of the level set is open by The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, so the level set is closed. If , the point is in the level set, and the set is its translate of ; every decomposes as with the first term in . Thus it is an affine hyperplane of the underlying real space.
Source notes
Brezis §1.2 definitions, pp.4–5; Teschl Theorems 5.2–5.3, pp.138–139.
Depends on
- Complex norm and complex normed space
- The dual space X^* of a normed space and its dual norm
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- Realification preserves a complex norm and its metric
Used by
- Nearest-point maps to convex sets need not be linear Counterexample
- The finite gauge of an open convex neighbourhood of zero Definition
- Quantitative separation of a norm ball from an exterior point Example
- A minimizing sequence in a convex set is Cauchy Lemma
- Banach mean value estimate on a convex set Lemma
- The projection onto a closed convex set is characterised by a variational inequality Lemma
- Uniform convexity gives unique asymptotic centers Lemma
- Projection onto a nonempty closed convex set Theorem
- Relative geometric Hahn–Banach with the exact open, closed, and compact hypotheses Theorem
- SLn(R) has property (T) for n at least three Theorem
- Variational characterisation of the nearest point Theorem
Dependency tree · two levels
24 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
- Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, §§1.1–1.2 and §1.3 evaluation paragraph (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis, Theorems 4.13–4.20 and §5.1 (2018 university-hosted copy) (standard reference, not scraped)