English
Repeated/distributed sum-product equivalence on the right: (α ⊕ β) × (γ ⊕ δ) ≃ᵐ ((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ)).
Русский
Повторное распределение по суммам и произведениям справа: (α ⊕ β) × (γ ⊕ δ) ≃ᵐ ((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ)).
LaTeX
$$$ (\alpha \oplus \beta) \times (\gamma \oplus \delta) \simeq^ᵐ ((\alpha \times \gamma) \oplus (\alpha \times \delta)) \oplus ((\beta \times \gamma) \oplus (\beta \times \delta)) $$$
Lean4
/-- A family of measurable equivalences `Π a, β₁ a ≃ᵐ β₂ a` generates a measurable equivalence
between `Π a, β₁ a` and `Π a, β₂ a`. -/
def piCongrRight (e : ∀ a, π a ≃ᵐ π' a) : (∀ a, π a) ≃ᵐ ∀ a, π' a
where
toEquiv := .piCongrRight fun a => (e a).toEquiv
measurable_toFun := measurable_pi_lambda _ fun i => (e i).measurable_toFun.comp (measurable_pi_apply i)
measurable_invFun := measurable_pi_lambda _ fun i => (e i).measurable_invFun.comp (measurable_pi_apply i)
