smul_measure — Mathlib

English

If f preserves μa to μb, then for any scalar c, f preserves c • μa to c • μb.

Русский

Если f сохраняет меру μa в μb, то для любого скаляра c мера c • μa отображается в c • μb посредством f.

LaTeX

$$$\\text{MeasurePreserving } f\\ μ_a\\ μ_b \\Rightarrow \\forall c,\\ \\text{MeasurePreserving } f\\ (c \\cdot μ_a)\\ (c \\cdot μ_b)$$$

Lean4

theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] {f : α → β} (hf : MeasurePreserving f μa μb)
    (c : R) : MeasurePreserving f (c • μa) (c • μb)
    where
  measurable := hf.measurable
  map_eq := by rw [Measure.map_smul, hf.map_eq]

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