smul — Mathlib

English

Scaling a regular measure preserves outer regularity, provided the scale is finite.

Русский

Умножение регулярной меры сохраняет внешнюю регулярность, если масштаб конечен.

LaTeX

$$$OuterRegular(\mu) \Rightarrow OuterRegular( x\cdot\mu)$ при $x\neq \infty$.$$

Lean4

protected theorem smul (μ : Measure α) [OuterRegular μ] {x : ℝ≥0∞} (hx : x ≠ ∞) : (x • μ).OuterRegular :=
  by
  rcases eq_or_ne x 0 with (rfl | h0)
  · rw [zero_smul]
    exact OuterRegular.zero
  · refine ⟨fun A _ r hr => ?_⟩
    rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr
    simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using hr

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