theorem subset_of_supportFunction_le_on_domain {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q₁ Q₂ : Set E) (hQ₂_nonempty : Q₂.Nonempty) (hQ₂_closed : IsClosed Q₂) (hQ₂_convex : Convex ℝ Q₂) (hξ : ∀ g ∈ extendedRealEffectiveDomain (supportFunction Q₂), supportFunction Q₁ g ≤ supportFunction Q₂ g) : Q₁ ⊆ Q₂

Theorem 3.17 (1): if Q₂ is a nonempty closed convex subset of a real Hilbert space and the support function of Q₁ is bounded above by that of Q₂ at every vector in dom ξ[Q₂], then Q₁ ⊆ Q₂.

theorem supportFunction_eq_on_common_domain_implies_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q₁ Q₂ : Set E) (hQ₁_closed : IsClosed Q₁) (hQ₂_closed : IsClosed Q₂) (hQ₁_convex : Convex ℝ Q₁) (hQ₂_convex : Convex ℝ Q₂) (hdom : extendedRealEffectiveDomain (supportFunction Q₁) = extendedRealEffectiveDomain (supportFunction Q₂)) (hξ : Set.EqOn (supportFunction Q₁) (supportFunction Q₂) (extendedRealEffectiveDomain (supportFunction Q₁))) : Q₁ = Q₂

Theorem 3.17 (2): if two closed convex sets in a real Hilbert space have the same effective domain for their support functions and those support functions agree on that common domain, then the sets are equal.