smul_measure — Mathlib

English

If f is quasi-preserving, then scaling both measures by a scalar c preserves quasi-measure-preservation.

Русский

Если f сохраняет, то умножение обеих мер на скаляр c сохраняет квази-сохранение мер.

LaTeX

$$QuasiMeasurePreserving f μa μb → (∀ c, QuasiMeasurePreserving f (c • μa) (c • μb))$$

Lean4

theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (hf : QuasiMeasurePreserving f μa μb)
    (c : R) : QuasiMeasurePreserving f (c • μa) (c • μb) :=
  ⟨hf.1, by rw [Measure.map_smul]; exact hf.2.smul c⟩

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