Step
*
1
1
1
1
of Lemma
cube+-
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. I1 : fset(ℕ)
4. alpha : names(I) ⟶ Point(dM(I1))
5. x1 : Point(dM(I1))
6. x : ℕ
7. i ∈ I
8. x = i ∈ ℤ
⊢ x1 = (alpha x) ∈ Point(dM(I1))
BY
{ (D 2 THEN D 3 THEN Auto) }
Latex:
Latex:
1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  I1  :  fset(\mBbbN{})
4.  alpha  :  names(I)  {}\mrightarrow{}  Point(dM(I1))
5.  x1  :  Point(dM(I1))
6.  x  :  \mBbbN{}
7.  i  \mmember{}  I
8.  x  =  i
\mvdash{}  x1  =  (alpha  x)
By
Latex:
(D  2  THEN  D  3  THEN  Auto)
Home
Index