---

Step * of Lemma ws-constant

∀[a:ℚ]. ∀[p:FinProbSpace]. ∀[F:Outcome ─→ ℚ].  weighted-sum(p;F) = a ∈ ℚ supposing ∀x:Outcome. ((F x) = a ∈ ℚ)
BY
{ (RepUR ``weighted-sum finite-prob-space p-outcome`` 0 THEN Auto) }

1
1. a : ℚ
2. p : {p:ℚ List| (Σ0 ≤ i < ||p||. p[i] = 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)} 
3. F : ℕ||p|| ─→ ℚ
4. ∀x:ℕ||p||. ((F x) = a ∈ ℚ)
⊢ Σ0 ≤ i < ||p||. (F i) * p[i] = a ∈ ℚ

---

Latex:


\mforall{}[a:\mBbbQ{}].  \mforall{}[p:FinProbSpace].  \mforall{}[F:Outcome  {}\mrightarrow{}  \mBbbQ{}].
    weighted-sum(p;F)  =  a  supposing  \mforall{}x:Outcome.  ((F  x)  =  a)


By

(RepUR  ``weighted-sum  finite-prob-space  p-outcome``  0  THEN  Auto)

---

Home Index