---

Step * of Lemma rat-cube-dimension-zero

∀[k:ℕ]. ∀[c:ℚCube(k)].  uiff(dim(c) = 0 ∈ ℤ;∀i:ℕk. ((fst((c i))) = (snd((c i))) ∈ ℚ))
BY
{ ((RWO "rat-cube-dimension-0" 0 THENA Auto)
   THEN RWO "assert-inhabited-rat-cube" 0
   THEN Auto
   THEN ∀h:hyp. ((InstHyp [⌜i⌝] h⋅ THENA Auto) THEN MoveToConcl (-1)) 
   THEN (GenConclTerm ⌜c i⌝⋅ THENA Auto)
   THEN All  Thin
   THEN D -1
   THEN RepUR ``inhabited-rat-interval rat-interval-dimension`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Try ((AutoSplit THEN RWO "qless_complement_qorder" (-1)))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].    uiff(dim(c)  =  0;\mforall{}i:\mBbbN{}k.  ((fst((c  i)))  =  (snd((c  i)))))


By

---

Latex:
((RWO  "rat-cube-dimension-0"  0  THENA  Auto)
  THEN  RWO  "assert-inhabited-rat-cube"  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  MoveToConcl  (-1)) 
  THEN  (GenConclTerm  \mkleeneopen{}c  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All    Thin
  THEN  D  -1
  THEN  RepUR  ``inhabited-rat-interval  rat-interval-dimension``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Try  ((AutoSplit  THEN  RWO  "qless\_complement\_qorder"  (-1)))
  THEN  Auto)

---

Home Index