sumProdSum — Mathlib

English

Products distribute over sums 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

/-- Products distribute over sums as measurable spaces. -/
def sumProdSum (α β γ δ) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] :
    (α ⊕ β) × (γ ⊕ δ) ≃ᵐ ((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ)) :=
  (sumProdDistrib _ _ _).trans <| sumCongr (prodSumDistrib _ _ _) (prodSumDistrib _ _ _)

Похожие утверждения