mapRange_add — Mathlib

English

MapRange is additive: mapRange f hf (g1 + g2) = mapRange f hf g1 + mapRange f hf g2.

Русский

MapRange является аддитивным: mapRange f hf (g1+g2) = mapRange f hf g1 + mapRange f hf g2.

LaTeX

$$$\\mathrm{mapRange}\, f\\, hf\\, (g_1 + g_2) = \\mathrm{mapRange}\\, f\\, hf\\, g_1 + \\mathrm{mapRange}\\, f\\, hf\\, g_2$$$

Lean4

theorem mapRange_add (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (hf' : ∀ i x y, f i (x + y) = f i x + f i y)
    (g₁ g₂ : Π₀ i, β₁ i) : mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂ :=
  by
  ext
  simp only [mapRange_apply f, coe_add, Pi.add_apply, hf']

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