gaugeRescale_smul — Mathlib

English

The gauge rescale map is positively homogeneous: for any nonnegative c, gaugeRescale s t (c x) = c · gaugeRescale s t x.

Русский

Положительная однородность: для неотрицательного c выполняется gaugeRescale s t (c x) = c · gaugeRescale s t x.

LaTeX

$$$0 \\le c \\Rightarrow \\operatorname{gaugeRescale}(s,t,c\\cdot x) = c \\cdot \\operatorname{gaugeRescale}(s,t,x)$$$

Lean4

theorem gaugeRescale_smul (s t : Set E) {c : ℝ} (hc : 0 ≤ c) (x : E) :
    gaugeRescale s t (c • x) = c • gaugeRescale s t x :=
  by
  simp only [gaugeRescale, gauge_smul_of_nonneg hc, smul_smul, smul_eq_mul]
  rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]

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