---

Step * 1 2 1 of Lemma boundary-singleton-complex


1. k : ℕ
2. n : ℕ
3. c : ℚCube(k)
4. dim(c) = n ∈ ℤ
⊢ ↑Inhabited(c)
BY
{ ((Unfold `rat-cube-dimension` -1 THEN SplitOnHypITE -1 ) THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  c  :  \mBbbQ{}Cube(k)
4.  dim(c)  =  n
\mvdash{}  \muparrow{}Inhabited(c)


By

---

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

---

Home Index