noncomputable def minkowskiGauge {H : Type u} [SMul ℝ H] (C : Set H) : H → EReal

Text 8.0.2: the Minkowski gauge of a subset C is the ]-∞,+∞]-valued function sending x to the infimum of the positive real numbers ξ such that x ∈ ξ C.

def «termM[_]» : Lean.ParserDescr

theorem minkowskiGauge_eq_sInf {H : Type u} [SMul ℝ H] (C : Set H) (x : H) : m[C] x = sInf (Real.toEReal '' {ξ : ℝ | 0 < ξ ∧ x ∈ ξ • C})

The textbook Minkowski gauge is the infimum of the positive real scalings that contain the point.