English
Let μ be a measure and s a set such that μ is everywhere positive on s. Then for every nonzero NNReal scalar c, the scaled measure c • μ is everywhere positive on s.
Русский
Пусть μ — мера, а s — множество, для которого μ является повсюду положительной на s. Тогда для любого ненулевого коэффициента c ∈ ℝ≥0, масштабирующая мера c • μ также имеет повсюду положительную меру на s.
LaTeX
$$$IsEverywherePos(\mu, s) \;
ightarrow\; \forall c \in \mathbb{R}_{\ge 0}, c \neq 0 \rightarrow IsEverywherePos(c \cdot \mu, s)$$$
Lean4
theorem smul_measure_nnreal (hs : IsEverywherePos μ s) {c : ℝ≥0} (hc : c ≠ 0) : IsEverywherePos (c • μ) s :=
hs.smul_measure (by simpa using hc)