---

Step * of Lemma meq-in-0-dim-cube

∀[k:ℕ]. ∀[c:ℚCube(k)].  ∀[p,q:ℝ^k].  (p ≡ q) supposing (in-rat-cube(k;q;c) and in-rat-cube(k;p;c)) supposing dim(c) = 0 \000C∈ ℤ
BY
{ (InstLemma `in-0-dim-cube` [] THEN RepeatFor 3 (ParallelLast')) }

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

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].
    \mforall{}[p,q:\mBbbR{}\^{}k].    (p  \mequiv{}  q)  supposing  (in-rat-cube(k;q;c)  and  in-rat-cube(k;p;c))  supposing  dim(c)  =  0


By

---

Latex:
(InstLemma  `in-0-dim-cube`  []  THEN  RepeatFor  3  (ParallelLast'))

---

Home Index