gauge_smul — Mathlib

English

If s is balanced and under suitable scalar-tower hypotheses, gauge(s) under r • x equals ‖r‖ times gauge s x.

Русский

Если s сбалансировано и соблюдены подходящие условия башни скаляров, gauge(s) под r • x равняется ‖r‖ умножить gauge s x.

LaTeX

$$$$\\mathrm{gauge}(s, r\\cdot x) = \\|r\\| \\cdot \\mathrm{gauge}(s,x).$$$$

Lean4

/-- If `s` is balanced, then the Minkowski functional is ℂ-homogeneous. -/
theorem gauge_smul (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (r • x) = ‖r‖ * gauge s x := by
  rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]

Похожие утверждения