dominatedFinMeasAdditive_weightedSMul

English

If x is nonnegative, then weightedSMul μ s x is nonnegative.

Русский

Если x неотрицательно, то weightedSMul μ s x неотрицательно.

LaTeX

$$$$0 \le weightedSMul \mu s x \quad\text{for } x \ge 0.$$$$

Lean4

theorem dominatedFinMeasAdditive_weightedSMul {_ : MeasurableSpace α} (μ : Measure α) :
    DominatedFinMeasAdditive μ (weightedSMul μ : Set α → F →L[ℝ] F) 1 :=
  ⟨weightedSMul_union, fun s _ _ => (norm_weightedSMul_le s).trans (one_mul _).symm.le⟩

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