isMulRightInvariant_smul — Mathlib

English

For any IsMulRightInvariant μ, the NNReal-scalar smul preserves right invariance: (c • μ) is right-invariant for c ∈ NNReal.

Русский

Для μ инвариантной справа, умножение на NNReal сохраняет инвариантность справа: c • μ инвариантна справа.

LaTeX

$$$[IsMulRightInvariant\\, \\mu] \\Rightarrow [IsMulRightInvariant\\, (c \\cdot \\mu)]$$$

Lean4

@[to_additive MeasureTheory.isAddRightInvariant_smul]
instance isMulRightInvariant_smul [IsMulRightInvariant μ] (c : ℝ≥0∞) : IsMulRightInvariant (c • μ) :=
  ⟨fun g => by rw [Measure.map_smul, map_mul_right_eq_self]⟩

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