theorem supportFunctionPrimal_le_of_inner_sub_nonpos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (B : Set E) (u p : E) (hsep : ∀ b ∈ B, inner ℝ u (b - p) ≤ 0) : σ[B] u ≤ ↑(inner ℝ u p)

Helper for Lemma 2.6: an inner-product upper bound on every b ∈ B yields the corresponding upper bound on the primal support function σ[B].

theorem existsSupportFunctionGapOfMemNotMemClosedConvex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A B : Set E) {x : E} (hxA : x ∈ A) (hxB : x ∉ B) (hB_nonempty : B.Nonempty) (hB_closed : IsClosed B) (hB_convex : Convex ℝ B) : ∃ (u : E), σ[B] u < σ[A] u

Helper for Lemma 2.6: a point of A lying outside a nonempty closed convex set B produces some direction whose primal support function is strictly larger on A than on B.

theorem subset_of_support_function_eq_of_closed_convex_right {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A B : Set E) (hB_closed : IsClosed B) (hB_convex : Convex ℝ B) (hσ : σ[A] = σ[B]) : A ⊆ B

Helper for Lemma 2.6: if two primal support functions agree and the right-hand set is closed and convex, then the left-hand set is contained in the right-hand set.

theorem eq_iff_support_function_eq_of_closed_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A B : Set E) (hA_closed : IsClosed A) (hA_convex : Convex ℝ A) (hB_closed : IsClosed B) (hB_convex : Convex ℝ B) : A = B ↔ σ[A] = σ[B]

Lemma 2.6: two closed convex sets in a real inner product space are equal if and only if their primal-space support functions σ[A] and σ[B] agree. This uses the chapter owner support_function_primal, the source-facing specialization of support_function along InnerProductSpace.toDualMap; the finite-dimensional Euclidean hypothesis supplies the Fréchet-Riesz identification with the continuous dual used in the converse direction.

theorem eq_of_support_function_eq_of_closed_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A B : Set E) (hA_closed : IsClosed A) (hA_convex : Convex ℝ A) (hB_closed : IsClosed B) (hB_convex : Convex ℝ B) (hσ : σ[A] = σ[B]) : A = B

Converse direction of Lemma 2.6, exposed as a direct callable theorem: equality of the primal-space support functions of two closed convex sets forces equality of the sets.