instSMul — Mathlib

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 _) }⟩

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