def «termσ[_]» : Lean.ParserDescr

theorem supportFunction_eq_sSup_image {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] (C : Set 𝓗) (u : 𝓗) : σ[C] u = sSup ((fun (x : 𝓗) => ↑(inner ℝ x u)) '' C)

The support function σ[C] is the supremum of the image of C under the functional x ↦ ⟪x, u⟫.

theorem ERealFunction.bot_lt_supportFunction_of_nonempty {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] (C : Set 𝓗) (hC_nonempty : C.Nonempty) (u : 𝓗) : ⊥ < σ[C] u

The support function of a nonempty set never takes the value -∞.

theorem ERealFunction.isProper_supportFunction_of_nonempty {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] (C : Set 𝓗) (hC_nonempty : C.Nonempty) : IsProper σ[C]

The support function of a nonempty set is proper as an EReal-valued function.