single_add — Mathlib

English

For all i, b1, b2 ∈ β i, single i (b1 + b2) = single i b1 + single i b2.

Русский

Для всех i, b1, b2 ∈ β i, одиночка на сумму равна сумме одиночек: single i (b1 + b2) = single i b1 + single i b2.

LaTeX

$$$ \\mathrm{single}_i (b_1 + b_2) = \\mathrm{single}_i b_1 + \\mathrm{single}_i b_2 $$$

Lean4

@[simp]
theorem single_add (i : ι) (b₁ b₂ : β i) : single i (b₁ + b₂) = single i b₁ + single i b₂ :=
  (zipWith_single_single (fun _ => (· + ·)) _ b₁ b₂).symm

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