smul_nnreal — Mathlib

English

If μ is a weakly regular measure on a measurable space, then for every c ≥ 0 in ℝ≥0, the scaled measure c • μ is weakly regular.

Русский

Если μ — слаборегулярная мера на измеримом пространстве, то для каждого c ≥ 0 в ℝ≥0 масштабированная мера c • μ также слаборегулярна.

LaTeX

$$$\\text{WeaklyRegular}(\\mu) \\Rightarrow \\forall c \\in \\mathbb{R}_{\\ge 0}, \\text{WeaklyRegular}(c\\,\\mu)$$$

Lean4

instance smul_nnreal [WeaklyRegular μ] (c : ℝ≥0) : WeaklyRegular (c • μ) :=
  WeaklyRegular.smul coe_ne_top

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