Step * of Lemma dot-product-split-first

[n:ℕ+]. ∀[x,y:ℝ^n].  (x⋅(((x 0) (y 0)) + λi.(x (i 1))⋅λi.(y (i 1))))
BY
(Intros THEN Unhide) }

1
.....wf..... 
1. : ℕ+
2. : ℝ^n
3. : ℝ^n
⊢ x⋅y ∈ ℝ

2
.....wf..... 
1. : ℕ+
2. : ℝ^n
3. : ℝ^n
⊢ ((x 0) (y 0)) + λi.(x (i 1))⋅λi.(y (i 1)) ∈ ℝ

3
1. : ℕ+
2. : ℝ^n
3. : ℝ^n
⊢ x⋅(((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