English
The product of finite spanning sets in α and β yields finite spanning sets in the product space for μ × ν in rectangles.
Русский
Произведение конечных охватывающих наборов в α и β образует конечные охватывающие наборы в произведении пространства для меры μ × ν.
LaTeX
$$FiniteSpanningSetsIn.prod$$
Lean4
/-- `μ.prod ν` has finite spanning sets in rectangles of finite spanning sets. -/
noncomputable def prod {ν : Measure β} {C : Set (Set α)} {D : Set (Set β)} (hμ : μ.FiniteSpanningSetsIn C)
(hν : ν.FiniteSpanningSetsIn D) : (μ.prod ν).FiniteSpanningSetsIn (image2 (· ×ˢ ·) C D) :=
by
haveI := hν.sigmaFinite
refine
⟨fun n => hμ.set n.unpair.1 ×ˢ hν.set n.unpair.2, fun n => mem_image2_of_mem (hμ.set_mem _) (hν.set_mem _), fun n =>
?_, ?_⟩
· rw [prod_prod]
exact mul_lt_top (hμ.finite _) (hν.finite _)
· simp_rw [iUnion_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ]
