isMulLeftInvariant_smul_nnreal — Mathlib

English

For any IsMulLeftInvariant μ, the NNReal-scalar smul preserves left invariance: (c • μ) IsMulLeftInvariant.

Русский

Для μ с инвариантностью слева, умножение на NNReal сохраняет инвариантность слева.

LaTeX

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

Lean4

@[to_additive MeasureTheory.isAddLeftInvariant_smul_nnreal]
instance isMulLeftInvariant_smul_nnreal [IsMulLeftInvariant μ] (c : ℝ≥0) : IsMulLeftInvariant (c • μ) :=
  MeasureTheory.isMulLeftInvariant_smul (c : ℝ≥0∞)

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