English
There is a measurable equivalence between the space of functions on a sum δ ⊕ δ′ and the product of two pi-types: one on the left piece δ → α (Sum.inl i) and one on the right δ′ → α (Sum.inr i′).
Русский
Существует измеримая эквивалентность между пространством функций на сумму δ ⊕ δ′ и произведением двух pi-типов: δ → α (Sum.inl i) и δ′ → α (Sum.inr i′).
LaTeX
$$$ (\\forall i:\\, δ\\oplus δ', \\alpha i) \\simeq^m (\\forall i:\\, δ, \\alpha(\\mathrm{Sum.inl}\\ i)) \\times (\\forall i':\\, δ', \\alpha(\\mathrm{Sum.inr}\\ i')) $$$
Lean4
/-- The measurable equivalence between the pi type over a sum type and a product of pi-types.
This is similar to `MeasurableEquiv.piEquivPiSubtypeProd`. -/
def sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
(∀ i, α i) ≃ᵐ (∀ i, α (.inl i)) × ∀ i', α (.inr i')
where
__ := Equiv.sumPiEquivProdPi α
measurable_toFun := by apply Measurable.prod <;> rw [measurable_pi_iff] <;> rintro i <;> apply measurable_pi_apply
measurable_invFun := by
rw [measurable_pi_iff]; rintro (i | i)
· exact measurable_pi_iff.1 measurable_fst _
· exact measurable_pi_iff.1 measurable_snd _
