measureReal_prod_prod — Mathlib

English

Equivalently, the real-valued product measure evaluates a rectangle by the product of the real measures of its sides.

Русский

Эквивалентно: действительная мера прямоугольника равна произведению действительных мер его граней.

LaTeX

$$$\mathrm{real}(s \timesˢ t) = \mathrm{real}(s) \cdot \mathrm{real}(t)$$$

Lean4

@[simp]
theorem _root_.MeasureTheory.measureReal_prod_prod (s : Set α) (t : Set β) :
    (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t := by simp only [measureReal_def, prod_prod, ENNReal.toReal_mul]

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