---

Step * 1 of Lemma positive-rat-cube-immediate-face

.....rewrite subgoal..... 
1. ∀k:ℕ. ∀c:ℚCube(k).  (0 < dim(c) ⇒ (∃i:ℕk. (dim(c i) = 1 ∈ ℤ)))
2. k : ℕ
3. ∀c:ℚCube(k). (0 < dim(c) ⇒ (∃i:ℕk. (dim(c i) = 1 ∈ ℤ)))
4. c : ℚCube(k)
5. 0 < dim(c)
6. i : ℕk
7. dim(c i) = 1 ∈ ℤ
⊢ ↑Inhabited(c)
BY
{ (Unfold `rat-cube-dimension` -3 THEN SplitOnHypITE -3  THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  \mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).    (0  <  dim(c)  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}k.  (dim(c  i)  =  1)))
2.  k  :  \mBbbN{}
3.  \mforall{}c:\mBbbQ{}Cube(k).  (0  <  dim(c)  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}k.  (dim(c  i)  =  1)))
4.  c  :  \mBbbQ{}Cube(k)
5.  0  <  dim(c)
6.  i  :  \mBbbN{}k
7.  dim(c  i)  =  1
\mvdash{}  \muparrow{}Inhabited(c)


By

---

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

---

Home Index