sigma_add — Mathlib

English

For all t,u, s.sigma (λ a. t a + u a) = s.sigma t + s.sigma u.

Русский

Для всех t,u, s.sigma(λ a. t a + u a) = 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 sigma_add : ∀ t u : ∀ a, Multiset (σ a), (s.sigma fun a => t a + u a) = s.sigma t + s.sigma u :=
  Multiset.induction_on s (fun _ _ => rfl) fun a s IH t u =>
    by
    rw [cons_sigma, IH]
    simp [add_comm, add_left_comm, add_assoc]

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