Step * of Lemma extend-approx-ball_wf

[k,n:ℕ]. ∀[p:unit-ball-approx(n;k)]. ∀[z:{-k..k 1-}].
  extend-approx-ball(n;p;z) ∈ unit-ball-approx(n 1;k) supposing ((p i) (p i) i < n) (z z)) ≤ (k k)
BY
((Auto THEN MemTypeCD THEN Auto) THEN RepUR ``extend-approx-ball`` THEN Auto) }

1
1. : ℕ
2. : ℕ
3. unit-ball-approx(n;k)
4. {-k..k 1-}
5. ((p i) (p i) i < n) (z z)) ≤ (k k)
⊢ Σ(if i <then else fi  if i <then else fi  i < 1) ≤ (k k)


Latex:


Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[p:unit-ball-approx(n;k)].  \mforall{}[z:\{-k..k  +  1\msupminus{}\}].
    extend-approx-ball(n;p;z)  \mmember{}  unit-ball-approx(n  +  1;k) 
    supposing  (\mSigma{}((p  i)  *  (p  i)  |  i  <  n)  +  (z  *  z))  \mleq{}  (k  *  k)


By


Latex:
((Auto  THEN  MemTypeCD  THEN  Auto)  THEN  RepUR  ``extend-approx-ball``  0  THEN  Auto)




Home Index