---

Step * 1 of Lemma face-forall-q=0

.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. a : Gamma(I)
4. (∀new-name(I).(new-name(I)=0))
= if (new-name(I) =z new-name(I)) then 0 else (new-name(I)=0) fi 
∈ Point(face_lattice(I))
⊢ (∀new-name(I).(q=0)((s(a);<new-name(I)>))) = (∀new-name(I).(new-name(I)=0)) ∈ 𝔽(a)
BY
{ EqCDA }

1
.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. a : Gamma(I)
4. (∀new-name(I).(new-name(I)=0))
= if (new-name(I) =z new-name(I)) then 0 else (new-name(I)=0) fi 
∈ Point(face_lattice(I))
⊢ (q=0)((s(a);<new-name(I)>)) = (new-name(I)=0) ∈ Point(face_lattice(I+new-name(I)))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  Gamma  :  CubicalSet\{j\}
2.  I  :  fset(\mBbbN{})
3.  a  :  Gamma(I)
4.  (\mforall{}new-name(I).(new-name(I)=0))  =  if  (new-name(I)  =\msubz{}  new-name(I))  then  0  else  (new-name(I)=0)  fi 
\mvdash{}  (\mforall{}new-name(I).(q=0)((s(a);<new-name(I)>)))  =  (\mforall{}new-name(I).(new-name(I)=0))


By

---

Latex:
EqCDA

---

Home Index