English
Scalar multiplication on outer measures is defined by scaling the values of the measure: (c • m)(s) = c • m(s).
Русский
Умножение на скаляр на внешних мерах определяется масштабированием значений меры: (c • m)(s) = c • m(s).
LaTeX
$$$\forall c:\, R,\forall m:\, OuterMeasure\ \alpha,\forall s:\, Set\ \alpha,\ (c \cdot m)(s) = c \cdot m(s).$$$
Lean4
instance instSMul : SMul R (OuterMeasure α) :=
⟨fun c m =>
{ measureOf := fun s => c • m s
empty := by simp only [measure_empty]; rw [← smul_one_mul c]; simp
mono := fun {s t} h => by
rw [← smul_one_mul c, ← smul_one_mul c (m t)]
exact mul_right_mono (m.mono h)
iUnion_nat := fun s _ => by
simp_rw [← smul_one_mul c (m _), ENNReal.tsum_mul_left]
exact mul_right_mono (measure_iUnion_le _) }⟩