English
Let s be finite and t_i subsets with pairwise disjointness across i in s. If HasProd holds for each i in s on t_i with product a_i, then HasProd holds for the union across all t_i with product ∏ i∈s a_i.
Русский
Пусть s — конечное множество, t_i — подмножества с попарной несовпадаемостью по i, и HasProd выполняется для каждого i на t_i с произведением a_i; тогда HasProd выполняется на объединении ⋃ t_i с произведением ∏ a_i.
LaTeX
$$HasProd (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∏ i ∈ s, a i) L$$
Lean4
@[to_additive]
theorem hasProd_prod_disjoint {ι} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : (s : Set ι).Pairwise (Disjoint on t))
(hf : ∀ i ∈ s, HasProd (f ∘ (↑) : t i → α) (a i)) : HasProd (f ∘ (↑) : (⋃ i ∈ s, t i) → α) (∏ i ∈ s, a i) :=
by
simp_rw [hasProd_subtype_iff_mulIndicator] at *
rw [Finset.mulIndicator_biUnion _ _ hs]
exact hasProd_prod hf
