---

Step * 1 of Lemma half-cube-dimension

.....assertion..... 
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. h : ℚCube(k)
5. ∀i:ℕk. (↑is-half-interval(h i;c i))
⊢ ∀i:ℕk. (dim(h i) = dim(c i) ∈ ℤ)
BY
{ (ParallelLast THEN MoveToConcl (-1) THEN GenConclTerms Auto [⌜h i⌝;⌜c i⌝]⋅) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. h : ℚCube(k)
5. ∀i:ℕk. (↑is-half-interval(h i;c i))
6. i : ℕk
7. v : ℚInterval
8. (h i) = v ∈ ℚInterval
9. v1 : ℚInterval
10. (c i) = v1 ∈ ℚInterval
⊢ (↑is-half-interval(v;v1)) ⇒ (dim(v) = dim(v1) ∈ ℤ)

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  \muparrow{}Inhabited(c)
4.  h  :  \mBbbQ{}Cube(k)
5.  \mforall{}i:\mBbbN{}k.  (\muparrow{}is-half-interval(h  i;c  i))
\mvdash{}  \mforall{}i:\mBbbN{}k.  (dim(h  i)  =  dim(c  i))


By

---

Latex:
(ParallelLast  THEN  MoveToConcl  (-1)  THEN  GenConclTerms  Auto  [\mkleeneopen{}h  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{})

---

Home Index