theorem gaugeFunction_closed_and_level_sets {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) (hCabs : ∀ (x : Fin n → ℝ), ∃ (lam : ℝ), 0 ≤ lam ∧ x ∈ (fun (y : Fin n → ℝ) => lam • y) '' C) : have e := EuclideanSpace.equiv (Fin n) ℝ; have C' := ⇑e.symm '' C; have recC := ⇑e '' C'.recessionCone; (ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(gaugeFunction C x)) ∧ (∀ (lam : ℝ), 0 < lam → {x : Fin n → ℝ | gaugeFunction C x ≤ lam} = lam • C) ∧ {x : Fin n → ℝ | gaugeFunction C x = 0} = recC

Corollary 9.7.1. Let C be a closed convex set in ℝ^n containing 0. The gauge function gamma(· | C) of C is closed. One has {x | gamma(x | C) ≤ λ} = λ C for any λ > 0, and {x | gamma(x | C) = 0} = 0^+ C.