Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Relative geometric Hahn–Banach with the exact open, closed, and compact hypotheses

Statement

Assume HB. Let A,B be disjoint nonempty convex subsets of a real or complex normed space X.

(i) If A is open, there are 0≠f∈X∗ and a∈R with Re⁡f(x)<a≤Re⁡f(y)(x∈A, y∈B). If B is also open, the right inequality is strict too. If only B is open, interchange the labels and negate the functional to put the strict inequality on the B side.

(ii) If A is closed and B is compact, there are 0≠f∈X∗, a∈R, and ε>0 with Re⁡f(x)≤a−ε<a+ε≤Re⁡f(y)(x∈A, y∈B). In particular, a point outside a nonempty closed convex set is uniformly strictly separated from it. All inequalities concern real parts.

Facts & Assumptions

[F1]

Under HB a nonempty open convex set and an exterior point admit a nonzero bounded scalar-linear functional with strict real-part separation (Relative separation of an open convex set from an exterior point).

[F2]

A nonempty compact set and a disjoint nonempty closed set have a uniform positive norm-distance lower bound (A compact set and a disjoint closed set have a positive norm-distance gap).

[F3]

Convexity uses real weights; for 0≠f∈X∗, u=Re⁡f is a nonzero bounded real-linear functional, and a uniform positive margin defines uniform strict separation (Convex sets and continuous real-hyperplane separation in a normed space).

[F4]

A supremum of a nonempty upper-bounded real set has elements within every positive error from below (Epsilon characterisation of the supremum).

[F5]

A nonempty lower-bounded real set has a real infimum; reflection gives the corresponding real supremum (Every nonempty set bounded below has an infimum).

Proof

Given: HB, a normed real or complex X, and disjoint nonempty convex A,B, with the additional hypotheses of each part.

1.1givenF3algebra

For (i), put D=A−B={x−y:x∈A,y∈B}. It is nonempty. For xj−yj∈D and 0≤t≤1, their convex combination equals ((1−t)x1+tx2)−((1−t)y1+ty2)∈D. If x−y∈D, choose r>0 with B(x,r)⊆A; then B(x−y,r)⊆D by keeping y fixed. Thus D is open and convex. If 0∈D, then some x∈A equals some y∈B, contrary to disjointness; hence 0∉D.

1.2givenF2F3algebra

For (ii), now suppose A is closed and B compact. The distance-gap lemma applied with K=B,C=A gives δ>0 with ∥x−y∥≥δ for all x∈A,y∈B. Put ρ=δ/2 and O=A+B(0,ρ). The ball is convex by the triangle inequality, so for xj+hj∈O each convex combination has its A component in A and its ball component of norm less than ρ, including the weights zero and one. Thus O is convex. A ball about x+h of radius ρ−∥h∥ stays in O, so O is open; it contains nonempty A. If x+h=y∈B, then ∥x−y∥=∥h∥<ρ<δ, impossible. Therefore O and B are disjoint.

2.1step 1.1F1F3F5

For (i), apply point separation to D and 0. It gives 0≠f∈X∗ with u(d)<u(0)=0 for every d∈D, where u=Re⁡f is nonzero bounded real-linear. Consequently u(x)<u(y) for every x∈A,y∈B. Fix y0∈B. The nonempty real set u(A) is bounded above by u(y0), so it has a real supremum a0. Explicitly, a0=−inf⁡(−u(A)); reflection of lower bounds makes this the least upper bound. Since every u(y) bounds u(A), a0≤u(y) for all y∈B.

3.1step 2.1algebra

For (i), fix a vector v with u(v)>0: nonzero u has a nonzero value, and negation makes that value positive. For each fixed x∈A, choose rx>0 with B(x,rx)⊆A and set t=rx/(2∥v∥)>0. Then x+tv∈A and u(x)<u(x)+tu(v)=u(x+tv)≤a0. This proves the strict left inequality. If B is open, for each y∈B choose sy>0 with B(y,sy)⊆B and set t=sy/(2∥v∥). Then y−tv∈B, and step 2.1 gives a0≤u(y−tv)<u(y). Thus both inequalities are strict in that case.

4.1step 2.1step 3.1algebra

If only B is open, apply the result just proved to (B,A) to get a functional g and level b with Re⁡g(y)<b≤Re⁡g(x) for y∈B,x∈A. Taking f=−g and a=−b gives Re⁡f(x)≤a<Re⁡f(y). This completes (i) in each orientation.

4.2step 2.1step 3.1step 1.2F3

For (ii), apply the already proved open-side assertion to (O,B). It gives 0≠f∈X∗ and a0∈R with u(x)+u(h)<a0≤u(y) whenever x∈A, ∥h∥<ρ, and y∈B, where u=Re⁡f≠0. Regard u as a member of the real dual of the underlying normed space, and let N=∥u∥=sup⁡∥v∥≤1∣u(v)∣. The bound ∣u(v)∣≤∥f∥∥v∥ makes this supremum finite, and a normalized vector with nonzero value shows N>0.

5.1step 4.2F4algebra

Continuing (ii), we show sup⁡∥h∥<ρu(h)=ρN. Normalization gives u(h)≤∣u(h)∣≤N∥h∥≤ρN (including h=0). For any q<ρN with q<0, h=0 has u(h)>q. For 0≤q<ρN, use the supremum criterion for N with error N−q/ρ>0 to obtain v with ∥v∥≤1 and ∣u(v)∣>q/ρ. Let w=v if u(v)>0 and w=−v otherwise; then m=u(w)=∣u(v)∣>0. Set t=(q/m+ρ)/2, which satisfies 0<t<ρ and tm>q. Thus h=tw has ∥h∥<ρ and u(h)>q. No number smaller than ρN is an upper bound, proving the identity.

6.1step 4.2step 5.1F3algebra

For (ii), for each fixed x∈A, step 4.2 says a0−u(x) is an upper bound for all u(h) with ∥h∥<ρ. The identity just proved yields u(x)+ρN≤a0. Put ε=ρN/2>0 and a=a0−ε. Then u(x)≤a0−ρN=a−ε, while a+ε=a0≤u(y) for every y∈B. Since ε>0, these are precisely the required uniform strict separation inequalities.

7.1step 1.2step 6.1algebra∎

Finally, if z lies outside a nonempty closed convex A, the set B={z} is nonempty, disjoint from A, and convex since (1−t)z+tz=z. It is intrinsically compact: any open cover of its one-point metric space has a member containing z, and that one member is a finite subcover. Thus the hypotheses of (ii) hold and steps 1.2, 4.2, 5.1 and 6.1 give the final specialization.

Source notes

Brezis Theorems 1.6–1.7, pp.5–7; Teschl Theorems 5.2–5.3 and Corollary 5.4, pp.138–140.

Depends on

Used by

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