smul_measure_nnreal — Mathlib

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)

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