---

Step * of Lemma comp-nc-0-subset-I_cube

∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[phi:𝔽(I)].  ∀J:fset(ℕ). ∀[f:I,phi(J)]. ((i0) ⋅ f ∈ I+i,s(phi)(J))
BY
{ (Auto
   THEN (CubicalSubsetICube (-1) THENA Auto)
   THEN (CubicalSubsetICube 0 THENA Auto)
   THEN RWO "name-morph-satisfies-comp" 0
   THEN Auto
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
4:n
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. phi : 𝔽(I)
4. J : fset(ℕ)
5. f : I,phi(J)
6. f ∈ J ⟶ I
7. (phi f) = 1
⊢ s ⋅ (i0) ⋅ f = f ∈ J ⟶ I

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[phi:\mBbbF{}(I)].
    \mforall{}J:fset(\mBbbN{}).  \mforall{}[f:I,phi(J)].  ((i0)  \mcdot{}  f  \mmember{}  I+i,s(phi)(J))


By

---

Latex:
(Auto
  THEN  (CubicalSubsetICube  (-1)  THENA  Auto)
  THEN  (CubicalSubsetICube  0  THENA  Auto)
  THEN  RWO  "name-morph-satisfies-comp"  0
  THEN  Auto
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index