smul_measure — Mathlib

English

If μ is everywhere positive on s, then for any nonzero ENNReal scalar c, the measure c • μ is also everywhere positive on s.

Русский

Если μ everywherePos на s, то при любом ненулевом скаляре c мера c•μ тоже everywherePos на s.

LaTeX

$$$$ (\\text{IsEverywherePos } μ\\, s) \\Rightarrow (c\\,\\mu) \\text{ is everywhere pos on } s \\quad (c\\neq 0). $$$$

Lean4

theorem smul_measure (hs : IsEverywherePos μ s) {c : ℝ≥0∞} (hc : c ≠ 0) : IsEverywherePos (c • μ) s := fun x hx n hn ↦
  by simpa [hc.bot_lt, hs x hx n hn] using hc.bot_lt

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