---

Step * of Lemma in-0-dim-cube

∀[k:ℕ]. ∀[c:ℚCube(k)].  ∀[p:ℝ^k]. uiff(in-rat-cube(k;p;c);req-vec(k;p;λj.rat2real(fst((c j))))) supposing dim(c) = 0 ∈ ℤ
BY
{ (RepeatFor 3 (Intro) THEN (Unhide THENA Auto)) }

1
1. k : ℕ
2. c : ℚCube(k)
3. dim(c) = 0 ∈ ℤ
4. p : ℝ^k
⊢ SqStable(req-vec(k;p;λj.rat2real(fst((c j)))))

2
1. k : ℕ
2. c : ℚCube(k)
3. dim(c) = 0 ∈ ℤ
⊢ ∀[p:ℝ^k]. uiff(in-rat-cube(k;p;c);req-vec(k;p;λj.rat2real(fst((c j)))))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].
    \mforall{}[p:\mBbbR{}\^{}k].  uiff(in-rat-cube(k;p;c);req-vec(k;p;\mlambda{}j.rat2real(fst((c  j)))))  supposing  dim(c)  =  0


By

---

Latex:
(RepeatFor  3  (Intro)  THEN  (Unhide  THENA  Auto))

---

Home Index