Step
*
2
1
of Lemma
upper-rc-face-dimension
.....subterm..... T:t
1:n
1. k : ℕ
2. c : ℚCube(k)
3. j : ℕk
4. dim(c j) ≠ 0
5. ↑Inhabited(c j)
6. ∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. Σ(f[x] | x < n) = (f[j] + Σ(if (x =z j) then 0 else f[x] fi | x < n)) ∈ ℤ supposing j < n
7. dim(c j) = 1 ∈ ℤ
⊢ dim([snd((c j))]) = (dim(c j) - 1) ∈ ℤ
BY
{ (RWO "rat-interval-dimension-single" 0 THEN Auto) }
Latex:
Latex:
.....subterm..... T:t
1:n
1. k : \mBbbN{}
2. c : \mBbbQ{}Cube(k)
3. j : \mBbbN{}k
4. dim(c j) \mneq{} 0
5. \muparrow{}Inhabited(c j)
6. \mforall{}[n:\mBbbN{}]. \mforall{}[f:\mBbbN{}n {}\mrightarrow{} \mBbbZ{}].
\mSigma{}(f[x] | x < n) = (f[j] + \mSigma{}(if (x =\msubz{} j) then 0 else f[x] fi | x < n)) supposing j < n
7. dim(c j) = 1
\mvdash{} dim([snd((c j))]) = (dim(c j) - 1)
By
Latex:
(RWO "rat-interval-dimension-single" 0 THEN Auto)
Home
Index