English
There is a natural MeasurableEquiv between the restricted product s ×ˢ t (as a subspace of α × β) and the Cartesian product s × t, given by the standard product map with measurable structure.
Русский
Существует естественное измеримое эквивалентство между ограниченным произведением s ×ˢ t и обычным произведением s × t, заданное стандартной картой произведения с относимой измеримостной структурой.
LaTeX
$$$$ \\text{prod}(s,t) : (s \\times^{\\mathrm{s}} t) \\simeq^{\\mathsf{m}} s \\times t. $$$$
Lean4
/-- `s ×ˢ t ≃ (s × t)` as measurable spaces. -/
def prod (s : Set α) (t : Set β) : ↥(s ×ˢ t) ≃ᵐ s × t
where
toEquiv := Equiv.Set.prod s t
measurable_toFun := measurable_id.subtype_val.fst.subtype_mk.prodMk measurable_id.subtype_val.snd.subtype_mk
measurable_invFun := Measurable.subtype_mk <| measurable_id.fst.subtype_val.prodMk measurable_id.snd.subtype_val
