---

Step * of Lemma rat-cube-dimension-0

∀[k:ℕ]. ∀[c:ℚCube(k)].  uiff(dim(c) = 0 ∈ ℤ;(↑Inhabited(c)) ∧ (∀i:ℕk. (dim(c i) = 0 ∈ ℤ)))
BY
{ (Auto
   THEN ((Unfold `rat-cube-dimension` 3 THEN SplitOnHypITE 3  THEN Auto)
        ORELSE (Unfold `rat-cube-dimension` 0 THEN SplitOnConclITE THEN Auto)
        )
   ) }

1
.....truecase..... 
1. k : ℕ
2. c : ℚCube(k)
3. Σ(dim(c i) | i < k) = 0 ∈ ℤ
4. i : ℕk
5. ↑Inhabited(c)
⊢ dim(c i) = 0 ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((Unfold  `rat-cube-dimension`  3  THEN  SplitOnHypITE  3    THEN  Auto)
            ORELSE  (Unfold  `rat-cube-dimension`  0  THEN  SplitOnConclITE  THEN  Auto)
            )
  )

---

Home Index