product_add — Mathlib

English

For s a multiset and t,u functions from α to multisets, sigma distributes over addition: s.sigma(t+u) = s.sigma(t) + s.sigma(u).

Русский

Для множества s и функций t,u из α в множества σ, σ распределяется по сложению: s.sigma(t+u) = s.sigma(t) + s.sigma(u).

LaTeX

$$$\forall t,u:\ (s.\sigma (\lambda a. t a + u a)) = s.\sigma t + s.\sigma u$$$

Lean4

@[simp]
theorem product_add (s : Multiset α) : ∀ t u : Multiset β, s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u :=
  Multiset.induction_on s (fun _ _ => rfl) fun a s IH t u =>
    by
    rw [cons_product, IH]
    simp [add_left_comm, add_assoc]

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