English
Let s and t be disjoint subsets of β. If HasProd on s and on t hold with products a and b, then HasProd on s ∪ t holds with product a·b.
Русский
Пусть s и t — непересекающиеся множества подмножеств β. Если HasProd на s даёт произведение a, а на t — b, то HasProd на s ∪ t даёт произведение a b.
LaTeX
$$HasProd (f ∘ (↑) : (s ∪ t) → α) (a * b) L$$
Lean4
@[to_additive]
theorem hasProd_prod {f : γ → β → α} {a : γ → α} {s : Finset γ} :
(∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L := by
classical
exact
Finset.induction_on s (by simp only [hasProd_one, prod_empty, forall_true_iff]) <|
by
simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff, prod_insert, and_imp]
exact fun x s _ IH hx h ↦ hx.mul (IH h)
