LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Minimizer face of a continuous affine functional

Statement

Let $K$ be a nonempty compact convex subset of a real or complex topological vector space, and let $a : K \to R$ be continuous and affine for real convex combinations. Then $a$ attains its minimum $m$ , and

$F = {x \in K : a (x) = m}$

is a nonempty compact face of $K$ . Moreover, if $G$ is a face of $F$ , then $G$ is a face of $K$ .

Facts & Assumptions

Given: A nonempty compact convex set $K$ and a continuous real-valued affine map $a$ on $K$ .

[F1]

A continuous real-valued function on a nonempty compact space attains its minimum (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[F2]

A closed subset of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, claim 1).

[F3]

A face is a nonempty convex subset satisfying the strict endpoint condition (Extreme point and face).

Proof

technique · direct

1.1

By [F1], some $x_{0} \in K$ satisfies $a (x_{0}) = m : = \min_{x \in K} a (x)$ , so $F$ is nonempty. Since $F = a^{- 1} ({m})$ and $a$ is continuous, $F$ is closed in $K$ ; hence it is compact by [F2].

F1F2given

2.1

If $x, y \in F$ and $0 \leq t \leq 1$ , affinity gives $a ((1 - t) x + t y) = (1 - t) m + t m = m$ , so convexity of $K$ places the combination in $F$ ; thus $F$ is convex.

step 1.1given

2.2

Suppose $x, y \in K$ , $0 < t < 1$ , and $(1 - t) x + t y \in F$ . Minimality gives $a (x), a (y) \geq m$ , while affinity gives $(1 - t) a (x) + t a (y) = m$ ; the two positive coefficients force $a (x) = a (y) = m$ , so $x, y \in F$ . Therefore $F$ is a face by [F3].

F3step 1.1given

3.1

Let $G$ be a face of $F$ , and suppose $x, y \in K$ , $0 < t < 1$ , and $(1 - t) x + t y \in G$ . Since $G \subseteq F$ and $F$ is a face of $K$ , step 2.2 gives $x, y \in F$ ; the face condition for $G$ inside $F$ then gives $x, y \in G$ . Since $G$ is already nonempty and convex, [F3] makes it a face of $K$ .

F3step 2.2

4.1

Steps 1.1–2.2 prove that the minimum is attained and its level set is a nonempty compact face; step 3.1 proves that faces of faces are faces.

step 1.1step 2.1step 2.2step 3.1∎

Depends on

Used by

Krein–Milman closed-convex-hull form Theorem
Krein–Milman existence of extreme points 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

Bühler–Salamon, Functional Analysis (standard reference, not scraped)
Hanche-Olsen, Topological vector spaces (standard reference, not scraped)