Step * 1 of Lemma weighted-sum-linear


1. : ℚ
2. : ℚ
⊢ ∀[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
Assert ⌈∀n:ℕ. ∀F,G:ℕn ─→ ℚ. ∀p:ℚ List.
            ((||p|| ≤ n)
             (weighted-sum(p;λx.((a (F x)) (b (G x))))
               ((a weighted-sum(p;F)) (b weighted-sum(p;G)))
               ∈ ℚ))⌉⋅ }

1
.....assertion..... 
1. : ℚ
2. : ℚ
⊢ ∀n:ℕ. ∀F,G:ℕn ─→ ℚ. ∀p:ℚ List.
    ((||p|| ≤ n)
     (weighted-sum(p;λx.((a (F x)) (b (G x)))) ((a weighted-sum(p;F)) (b weighted-sum(p;G))) ∈ ℚ))

2
1. : ℚ
2. : ℚ
3. ∀n:ℕ. ∀F,G:ℕn ─→ ℚ. ∀p:ℚ List.
     ((||p|| ≤ n)
      (weighted-sum(p;λx.((a (F x)) (b (G x)))) ((a weighted-sum(p;F)) (b weighted-sum(p;G))) ∈ ℚ))
⊢ ∀[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:



1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
\mvdash{}  \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

Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}F,G:\mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}.  \mforall{}p:\mBbbQ{}  List.
                    ((||p||  \mleq{}  n)
                    {}\mRightarrow{}  (weighted-sum(p;\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
                          =  ((a  *  weighted-sum(p;F))  +  (b  *  weighted-sum(p;G)))))\mkleeneclose{}\mcdot{}




Home Index