isFiniteMeasureSMulOfNNRealTower — Mathlib

English

For any R with NNReal scalars, if μ is finite, then instHSMul.hSMul r μ is finite.

Русский

Для любого R со скалярами NNReal, если μ конечна, то instHSMul.hSMul r μ конечна.

LaTeX

$$IsFiniteMeasure (instHSMul.hSMul r μ)$$

Lean4

instance isFiniteMeasureSMulOfNNRealTower {R} [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0 ℝ≥0∞]
    [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [IsFiniteMeasure μ] {r : R} : IsFiniteMeasure (r • μ) :=
  by
  rw [← smul_one_smul ℝ≥0 r μ]
  infer_instance

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