English
If each space has finite volume, then the product space also has finite volume.
Русский
Если объёмы на пространствах конечны, то и их произведение имеет конечный объём.
LaTeX
$$$\text{volume}$ на $\alpha \times \beta$ конечна, если $\mathrm{volume}$ на $\alpha$ и $\beta$ конечны.$$
Lean4
instance instIsOpenPosMeasure {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {m : MeasurableSpace X}
{μ : Measure X} [IsOpenPosMeasure μ] {m' : MeasurableSpace Y} {ν : Measure Y} [IsOpenPosMeasure ν] [SFinite ν] :
IsOpenPosMeasure (μ.prod ν) := by
constructor
rintro U U_open ⟨⟨x, y⟩, hxy⟩
rcases isOpen_prod_iff.1 U_open x y hxy with ⟨u, v, u_open, v_open, xu, yv, huv⟩
refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono huv))
simp only [prod_prod, CanonicallyOrderedAdd.mul_pos]
constructor
· exact u_open.measure_pos μ ⟨x, xu⟩
· exact v_open.measure_pos ν ⟨y, yv⟩
