Theorems · Theorem · functional analysis

gauge_smul

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
  [inst_3 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E], Balanced 𝕜 s → ∀ (r : 𝕜) (x : E), gauge s (r • x) = ‖r‖ * gauge s x

If s is balanced, then the Minkowski functional is ℂ-homogeneous.

Defined in

Mathlib.Analysis.Convex.Gauge

Cited by

0 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModuleRCLikeModuleIsScalarTower