---

Step * 1 1 of Lemma face-zero-context-implies


1. X : CubicalSet{j}
2. i : {X ⊢ _:𝕀}
3. I : fset(ℕ)
4. a : X(I)
5. ¬(i I a) = 1 ∈ Point(dM(I))
⊢ (i I a) = (0(𝕀) I a) ∈ 𝕀(a)
BY
{ (RepUR ``interval-0`` 0 THEN MoveToConcl (-1)) }

1
1. X : CubicalSet{j}
2. i : {X ⊢ _:𝕀}
3. I : fset(ℕ)
4. a : X(I)
⊢ (¬(i I a) = 1 ∈ Point(dM(I))) ⇒ ((i I a) = 0 ∈ 𝕀(a))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``interval-0``  0  THEN  MoveToConcl  (-1))

---

Home Index