---

Step * of Lemma csm-ap-interval-1-adjoin-lemma

No Annotations
∀H:j⊢. ∀I:fset(ℕ). ∀v:H(I). ∀j:{i:ℕ| ¬i ∈ I} .  ((j1)((s(v);<j>)) = ([1(𝕀)])v ∈ H.𝕀(I))
BY
{ Auto }

1
1. H : CubicalSet{j}
2. I : fset(ℕ)
3. v : H(I)
4. j : {i:ℕ| ¬i ∈ I} 
⊢ (j1)((s(v);<j>)) = ([1(𝕀)])v ∈ H.𝕀(I)

---

Latex:

---

Latex:
No  Annotations
\mforall{}H:j\mvdash{}.  \mforall{}I:fset(\mBbbN{}).  \mforall{}v:H(I).  \mforall{}j:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  .    ((j1)((s(v);<j>))  =  ([1(\mBbbI{})])v)


By

---

Latex:
Auto

---

Home Index