---

Step * of Lemma rat-cube-dimension_wf

∀[k:ℕ]. ∀[c:ℚCube(k)].  (dim(c) ∈ {-1..k + 1-})
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
⊢ (-1) ≤ Σ(dim(c i) | i < k)

2
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
⊢ Σ(dim(c i) | i < k) < k + 1

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].    (dim(c)  \mmember{}  \{-1..k  +  1\msupminus{}\})


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index