tprod_finset_bUnion_disjoint — Mathlib

English

For a finite family f i on β and Finset s with pairwise disjoint images of sets t i, the tprod over the union equals the finite product over i of the tprod over t i.

Русский

Для конечной семейства f_i на β и Finset s с попарно непересекающимися образами множеств t_i, т-продукт по объединению равен произведению т-продуктов по кажному t_i.

LaTeX

$$$\\forall s : Finset, {f : γ → β → α}, {t : γ → Set β}, (∀ i ∈ s, Multipliable (f i) L) →\\prod' x : ⋃ i ∈ s, t i, f x = ∏ i ∈ s, ∏' x : t i, f x$$$

Lean4

@[to_additive]
protected theorem tprod_finset_bUnion_disjoint {ι} {s : Finset ι} {t : ι → Set β}
    (hd : (s : Set ι).Pairwise (Disjoint on t)) (hf : ∀ i ∈ s, Multipliable (f ∘ (↑) : t i → α)) :
    ∏' x : ⋃ i ∈ s, t i, f x = ∏ i ∈ s, ∏' x : t i, f x :=
  (hasProd_prod_disjoint _ hd fun i hi ↦ (hf i hi).hasProd).tprod_eq

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