English
There is a natural measurable equivalence between the space of functions γ → (α × β) and the product of function spaces (γ → α) × (γ → β), given by the usual pairing map and its inverse.
Русский
Существует естественная измеримая эквивалентность между множеством функций γ → (α × β) и произведением пространств функций (γ → α) × (γ → β), задаваемая обычной операцией пары и её обратной.
LaTeX
$$$ (\\gamma \\to (\\alpha \\times \\beta)) \\\\cong^m (\\gamma \\to \\alpha) \\times (\\gamma \\to \\beta) $$$
Lean4
/-- The isomorphism `(γ → α × β) ≃ (γ → α) × (γ → β)` as a measurable equivalence. -/
def arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableSpace β] : (γ → α × β) ≃ᵐ (γ → α) × (γ → β)
where
__ := Equiv.arrowProdEquivProdArrow γ _ _
measurable_toFun := by
dsimp [Equiv.arrowProdEquivProdArrow]
fun_prop
measurable_invFun := by
dsimp [Equiv.arrowProdEquivProdArrow]
fun_prop
