theorem ERealFunction.sSup_image_closure_eq_of_lowerSemicontinuous {H : Type u} [TopologicalSpace H] {f : H → EReal} (hf : LowerSemicontinuous f) (C : Set H) : sSup (f '' closure C) = sSup (f '' C)

Proposition 11.1 (i): a lower semicontinuous function has the same supremum on a set and on its closure.

theorem ERealFunction.sSup_image_convexHull_eq_of_isConvex {H : Type u} [AddCommMonoid H] [Module ℝ H] {f : H → EReal} (hf : IsConvex f) (C : Set H) : sSup (f '' (convexHull ℝ) C) = sSup (f '' C)

Proposition 11.1 (ii): a convex function has the same supremum on a set and on its convex hull.

theorem supportFunction_closure_convexHull_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : Set H) : σ[closure ((convexHull ℝ) C)] = σ[C]

Proposition 11.1 (iii), supremum form: the support function is unchanged by closed convex hull.

theorem innerInfimumOn_closure_convexHull_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : Set H) (u : H) : innerInfimumOn (closure ((convexHull ℝ) C)) u = innerInfimumOn C u

Proposition 11.1 (iii), infimum form: the inner-product infimum is unchanged by closed convex hull.

theorem ERealFunction.sInf_image_closure_eq_of_mem_gammaZero_of_convex_of_effectiveDomain_inter_interior_nonempty {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H → ↑(Set.Ioi ⊥)} (hf : f ∈ Γ₀(H)) {C : Set H} (hC : Convex ℝ C) (hinter : (effectiveDomain f ∩ interior C).Nonempty) : sInf (Function.asEReal f '' closure C) = sInf (Function.asEReal f '' C)

Proposition 11.1 (iv): for f ∈ Γ₀(H), convexity of C, and a point of the effective domain inside interior C, the infimum of f is unchanged by passing from C to closure C.