smul_measure — Mathlib

English

For any c ≠ 0, ∞, FinMeasAdditive for μ and for c•μ are equivalent.

Русский

Для любой константы c ≠ 0, ∞ FinMeasAdditive μ и FinMeasAdditive c•μ эквивалентны.

LaTeX

$$FinMeasAdditive (c•μ) T ↔ FinMeasAdditive μ T$$

Lean4

theorem smul_measure (c : ℝ≥0∞) (hc_ne_zero : c ≠ 0) (hT : FinMeasAdditive μ T) : FinMeasAdditive (c • μ) T :=
  by
  refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT
  rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top]
  simp only [hc_ne_zero, true_and, Ne, not_false_iff]
  exact Or.inl hμs

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