---

Step * 1 1 of Lemma cube+-


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. I1 : fset(ℕ)
4. alpha : I1 ⟶ I
5. x1 : Point(dM(I1))
⊢ (λj.if (j =z i) then x1 else alpha j fi ) = alpha ∈ I1 ⟶ I
BY
{ ((All (Unfold `names-hom`) THEN (FunExt THENA Auto)) THEN Reduce 0 THEN AutoSplit) }

1
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 : names(I)
7. x = i ∈ ℤ
⊢ x1 = (alpha x) ∈ Point(dM(I1))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  I1  :  fset(\mBbbN{})
4.  alpha  :  I1  {}\mrightarrow{}  I
5.  x1  :  Point(dM(I1))
\mvdash{}  (\mlambda{}j.if  (j  =\msubz{}  i)  then  x1  else  alpha  j  fi  )  =  alpha


By

---

Latex:
((All  (Unfold  `names-hom`)  THEN  (FunExt  THENA  Auto))  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index