---

Step * of Lemma weighted-sum-linear

∀[a,b:ℚ]. ∀[p:ℚ List]. ∀[F,G:ℕ||p|| ─→ ℚ].
  (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ)
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. a : ℚ
2. b : ℚ
⊢ ∀[p:ℚ List]. ∀[F,G:ℕ||p|| ─→ ℚ].
    (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ)

---

Latex:


\mforall{}[a,b:\mBbbQ{}].  \mforall{}[p:\mBbbQ{}  List].  \mforall{}[F,G:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}].
    (weighted-sum(p;\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
    =  ((a  *  weighted-sum(p;F))  +  (b  *  weighted-sum(p;G))))


By

RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index