---

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

No Annotations
∀k:ℕ. ∀c:ℚCube(k).  (0 < dim(c) ⇒ (∃f:ℚCube(k). immediate-rc-face(k;f;c)))
BY
{ (InstLemma `positive-rat-cube-dimension` []
   THEN RepeatFor 3 (ParallelLast)
   THEN ExRepD
   THEN (D 0 With ⌜upper-rc-face(c;i)⌝  THENA Auto)
   THEN D 0
   THEN Auto
   THEN RWO  "upper-rc-face-dimension" 0
   THEN Auto) }

1
.....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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).    (0  <  dim(c)  {}\mRightarrow{}  (\mexists{}f:\mBbbQ{}Cube(k).  immediate-rc-face(k;f;c)))


By

---

Latex:
(InstLemma  `positive-rat-cube-dimension`  []
  THEN  RepeatFor  3  (ParallelLast)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}upper-rc-face(c;i)\mkleeneclose{}    THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  RWO    "upper-rc-face-dimension"  0
  THEN  Auto)

---

Home Index