---

Step * 1 1 of Lemma implies-member-rat-cube-faces

.....assertion..... 
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. f : ℚCube(k)
5. f ≤ c
6. dim(f) = (dim(c) - 1) ∈ ℤ
⊢ ∃y:ℕk. ((↑(dim(c y) =z 1)) ∧ (f ∈ [lower-rc-face(c;y); upper-rc-face(c;y)]))
BY
{ (UnfoldTopAb (-2)
   THEN Unfold `rat-cube-dimension` -1
   THEN (InstLemma `inhabited-rat-cube-face` [⌜k⌝;⌜c⌝;⌜f⌝]⋅ THENA Auto)
   THEN (Subst' Inhabited(c) ~ tt -2 THENA Auto)
   THEN (Subst' Inhabited(f) ~ tt -2 THENA Auto)
   THEN Reduce -2) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. f : ℚCube(k)
5. ∀i:ℕk. f i ≤ c i
6. Σ(dim(f i) | i < k) = (Σ(dim(c i) | i < k) - 1) ∈ ℤ
7. ↑Inhabited(f)
⊢ ∃y:ℕk. ((↑(dim(c y) =z 1)) ∧ (f ∈ [lower-rc-face(c;y); upper-rc-face(c;y)]))

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  \muparrow{}Inhabited(c)
4.  f  :  \mBbbQ{}Cube(k)
5.  f  \mleq{}  c
6.  dim(f)  =  (dim(c)  -  1)
\mvdash{}  \mexists{}y:\mBbbN{}k.  ((\muparrow{}(dim(c  y)  =\msubz{}  1))  \mwedge{}  (f  \mmember{}  [lower-rc-face(c;y);  upper-rc-face(c;y)]))


By

---

Latex:
(UnfoldTopAb  (-2)
  THEN  Unfold  `rat-cube-dimension`  -1
  THEN  (InstLemma  `inhabited-rat-cube-face`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  Inhabited(c)  \msim{}  tt  -2  THENA  Auto)
  THEN  (Subst'  Inhabited(f)  \msim{}  tt  -2  THENA  Auto)
  THEN  Reduce  -2)

---

Home Index