---

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


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)))))
BY
{ ((RWO "rat-cube-dimension-zero" (-1) THENA Auto) THEN RepUR ``in-rat-cube req-vec`` 0 THEN RWO "-1" 0 THEN Auto) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. ((fst((c i))) = (snd((c i))) ∈ ℚ)
4. p : ℝ^k
5. ∀i:ℕk. ((rat2real(snd((c i))) ≤ (p i)) ∧ ((p i) ≤ rat2real(snd((c i)))))
6. i : ℕk
⊢ (p i) = rat2real(snd((c i)))

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "rat-cube-dimension-zero"  (-1)  THENA  Auto)
  THEN  RepUR  ``in-rat-cube  req-vec``  0
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index