---

Step * of Lemma half-cube-dimension

No Annotations
∀[k:ℕ]. ∀[c:{c:ℚCube(k)| ↑Inhabited(c)} ]. ∀[h:ℚCube(k)].  ((↑is-half-cube(k;h;c)) ⇒ (dim(h) = dim(c) ∈ ℤ))
BY
{ (Auto
   THEN DVar `c'
   THEN (RWO "assert-is-half-cube" (-1) THENA Auto)
   THEN Unfold `rat-cube-dimension` 0
   THEN (Subst' Inhabited(c) = tt 0 THENA Auto)
   THEN Reduce 0
   THEN Assert ⌜∀i:ℕk. (dim(h i) = dim(c i) ∈ ℤ)⌝⋅) }

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

2
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. (dim(h i) = dim(c i) ∈ ℤ)
⊢ if Inhabited(h) then Σ(dim(h i) | i < k) else -1 fi  = Σ(dim(c i) | i < k) ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}  ].  \mforall{}[h:\mBbbQ{}Cube(k)].
    ((\muparrow{}is-half-cube(k;h;c))  {}\mRightarrow{}  (dim(h)  =  dim(c)))


By

---

Latex:
(Auto
  THEN  DVar  `c'
  THEN  (RWO  "assert-is-half-cube"  (-1)  THENA  Auto)
  THEN  Unfold  `rat-cube-dimension`  0
  THEN  (Subst'  Inhabited(c)  =  tt  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Assert  \mkleeneopen{}\mforall{}i:\mBbbN{}k.  (dim(h  i)  =  dim(c  i))\mkleeneclose{}\mcdot{})

---

Home Index