---

Step * of Lemma req-vec-extend

∀[k:ℕ+]. ∀[a,b:ℝ^k - 1]. ∀[z,u:ℝ].  uiff(req-vec(k;a++z;b++u);(z = u) ∧ req-vec(k - 1;a;b))
BY
{ (Auto THEN Try (((D 0 THEN Auto) THEN RepUR ``real-vec-extend`` 0 THEN AutoSplit))) }

1
1. k : ℕ+
2. a : ℝ^k - 1
3. b : ℝ^k - 1
4. z : ℝ
5. u : ℝ
6. req-vec(k;a++z;b++u)
⊢ z = u

2
1. k : ℕ+
2. a : ℝ^k - 1
3. b : ℝ^k - 1
4. z : ℝ
5. u : ℝ
6. req-vec(k;a++z;b++u)
⊢ req-vec(k - 1;a;b)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[a,b:\mBbbR{}\^{}k  -  1].  \mforall{}[z,u:\mBbbR{}].    uiff(req-vec(k;a++z;b++u);(z  =  u)  \mwedge{}  req-vec(k  -  1;a;b))


By

---

Latex:
(Auto  THEN  Try  (((D  0  THEN  Auto)  THEN  RepUR  ``real-vec-extend``  0  THEN  AutoSplit)))

---

Home Index