Step
*
of Lemma
dot-product-split-first
∀[n:ℕ+]. ∀[x,y:ℝ^n].  (x⋅y = (((x 0) * (y 0)) + λi.(x (i + 1))⋅λi.(y (i + 1))))
BY
{ (Intros THEN Unhide) }
1
.....wf..... 
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
⊢ x⋅y ∈ ℝ
2
.....wf..... 
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
⊢ ((x 0) * (y 0)) + λi.(x (i + 1))⋅λi.(y (i + 1)) ∈ ℝ
3
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
⊢ x⋅y = (((x 0) * (y 0)) + λi.(x (i + 1))⋅λi.(y (i + 1)))
Latex:
Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (x\mcdot{}y  =  (((x  0)  *  (y  0))  +  \mlambda{}i.(x  (i  +  1))\mcdot{}\mlambda{}i.(y  (i  +  1))))
By
Latex:
(Intros  THEN  Unhide)
Home
Index