instMeasurableSMulNNReal — Mathlib

English

There is a MeasurableSMul NNReal → ENNReal, i.e., scalar multiplication is measurable in both directions.

Русский

Существует измеримая операция умножения NNReal на ENNReal.

LaTeX

$$$\text{MeasurableSMul NNReal ENNReal}$$$

Lean4

instance : MeasurableSMul ℝ≥0 ℝ≥0∞
    where
  measurable_const_smul _ := by simp_rw [ENNReal.smul_def]; exact measurable_const_smul _
  measurable_smul_const
    _ := by
    simp_rw [ENNReal.smul_def]
    exact measurable_coe_nnreal_ennreal.mul_const _

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