---

Step * of Lemma not-not-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 4 (Intro) THEN RWO "in-0-dim-cube" 0 THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(RepeatFor  4  (Intro)  THEN  RWO  "in-0-dim-cube"  0  THEN  Auto)

---

Home Index