smul — Mathlib

English

Multiplying a measure by a positive scalar preserves inner regularity with the same predicate families.

Русский

Умножение меры на положительный множитель сохраняет внутреннюю регулярность по тем же семействам предикатов.

LaTeX

$$$\text{If } InnerRegularWRT(\mu; p, q), \text{ then } InnerRegularWRT(c\cdot\mu; p, q)\text{ for any } c \in [0,\infty].$$$

Lean4

theorem smul (H : InnerRegularWRT μ p q) (c : ℝ≥0∞) : InnerRegularWRT (c • μ) p q :=
  by
  intro U hU r hr
  rw [smul_apply, H.measure_eq_iSup hU, smul_eq_mul] at hr
  simpa only [ENNReal.mul_iSup, lt_iSup_iff, exists_prop] using hr

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