instMeasurableSMul₂ENNReal — Mathlib

English

The multiplication map NNReal × ENNReal → ENNReal is measurable in the first argument, i.e. the bilinear map is measurable.

Русский

Вычисление умножения NNReal на ENNReal до ENNReal измеримо по аргументу из NNReal.

LaTeX

$$$\\operatorname{MeasurableSMul_2} \\; \\mathbb{R}_{\\ge 0} \\; \\mathbb{R}_{\\ge 0}^{\\infty}$$$

Lean4

instance : MeasurableSMul₂ ℝ≥0 ℝ≥0∞ where
  measurable_smul := show Measurable fun r : ℝ≥0 × ℝ≥0∞ ↦ (r.1 : ℝ≥0) * r.2 by fun_prop

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