---

Step * 1 2 of Lemma face-zero-eq-1


1. H : CubicalSet{j}
2. z : {H ⊢ _:𝕀}
3. I : fset(ℕ)
4. a : H(I)
5. ¬(z(a)) = 1 ∈ Point(dM(I))
6. ¬(¬(z(a))) = ¬(1) ∈ Point(dM(I))
⊢ z(a) = 0 ∈ 𝕀(a)
BY
{ (NthHypEq (-1) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  z  :  \{H  \mvdash{}  \_:\mBbbI{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  H(I)
5.  \mneg{}(z(a))  =  1
6.  \mneg{}(\mneg{}(z(a)))  =  \mneg{}(1)
\mvdash{}  z(a)  =  0


By

---

Latex:
(NthHypEq  (-1)  THEN  EqCD  THEN  Auto)

---

Home Index