weightedSMul_union — Mathlib

English

For any scalar c and x in F, the weightedSMul map commutes with scalar multiplication: weightedSMul μ s (c · x) = c · weightedSMul μ s x.

Русский

Для любого скаляра c и вектора x ∈ F, карта weightedSMul коммутирует умножение на скаляр: weightedSMul μ s (c · x) = c · weightedSMul μ s x.

LaTeX

$$$$weightedSMul μ s (c \cdot x) = c \cdot weightedSMul μ s x.$$$$

Lean4

@[nolint unusedArguments]
theorem weightedSMul_union (s t : Set α) (_hs : MeasurableSet s) (ht : MeasurableSet t) (hs_finite : μ s ≠ ∞)
    (ht_finite : μ t ≠ ∞) (hdisj : Disjoint s t) :
    (weightedSMul μ (s ∪ t) : F →L[ℝ] F) = weightedSMul μ s + weightedSMul μ t :=
  weightedSMul_union' s t ht hs_finite ht_finite hdisj

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