---

Step * of Lemma ws-linear

∀[a,b:ℚ]. ∀[p:FinProbSpace]. ∀[F,G:Outcome ⟶ ℚ].
  (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ)
BY
{ (InstLemma `weighted-sum-linear` []
   THEN RepeatFor 5 ((ParallelLast THENA ((All (Unfolds ``finite-prob-space p-outcome``))⋅ THEN Auto)))
   ) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `weighted-sum-linear`  []
  THEN  RepeatFor  5  ((ParallelLast
                                        THENA  ((All  (Unfolds  ``finite-prob-space  p-outcome``))\mcdot{}  THEN  Auto)
                                        ))
  )

---

Home Index