sumProdDistrib — Mathlib

English

Sums distribute over products: (α ⊕ β) × γ ≃ᵐ (α × γ) ⊕ (β × γ).

Русский

Суммы распределяются по произведениям: (α ⊕ β) × γ эквивалентно (α × γ) ⊕ (β × γ).

LaTeX

$$$ (\alpha \oplus \beta) \times \gamma \simeq^ᵐ (\alpha \times \gamma) \oplus (\beta \gamma) $$$

Lean4

/-- Products distribute over sums (on the right) as measurable spaces. -/
def sumProdDistrib (α β γ) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :
    (α ⊕ β) × γ ≃ᵐ (α × γ) ⊕ (β × γ) where
  toEquiv := .sumProdDistrib α β γ
  measurable_toFun :=
    by
    refine
      measurable_of_measurable_union_cover (range Sum.inl ×ˢ (univ : Set γ)) (range Sum.inr ×ˢ (univ : Set γ))
        (measurableSet_range_inl.prod MeasurableSet.univ) (measurableSet_range_inr.prod MeasurableSet.univ)
        (by rintro ⟨a | b, c⟩ <;> simp [Set.prod_eq]) ?_ ?_
    · refine (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 ?_
      refine (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 ?_
      exact measurable_inl
    · refine (Set.prod (range Sum.inr) univ).symm.measurable_comp_iff.1 ?_
      refine (prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 ?_
      exact measurable_inr
  measurable_invFun :=
    measurable_fun_sum ((measurable_inl.comp measurable_fst).prodMk measurable_snd)
      ((measurable_inr.comp measurable_fst).prodMk measurable_snd)

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