---

Step * of Lemma satisfies-s-face-lattice-tube

∀I:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀phi:𝔽(I). ∀j:{j:ℕ| ¬j ∈ I+i} . ∀K:fset(ℕ). ∀f:K ⟶ I+j+i.
  ((s(face-lattice-tube(I;phi;j)) f) = 1
  ⇐⇒ (s(phi) s ⋅ f) = 1 ∨ ((s ⋅ f j) = 0 ∈ Point(dM(K))) ∨ ((s ⋅ f j) = 1 ∈ Point(dM(K))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert s ⋅ f ∈ K ⟶ I+j BY
               Auto)
   THEN (RWO "name-morph-satisfies-comp" 0 THENA Auto)
   THEN RWO "satisfies-face-lattice-tube<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{}).  \mforall{}i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  .  \mforall{}phi:\mBbbF{}(I).  \mforall{}j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\}  .  \mforall{}K:fset(\mBbbN{}).  \mforall{}f:K  {}\mrightarrow{}  I+j+i.
    ((s(face-lattice-tube(I;phi;j))  f)  =  1  \mLeftarrow{}{}\mRightarrow{}  (s(phi)  s  \mcdot{}  f)  =  1  \mvee{}  ((s  \mcdot{}  f  j)  =  0)  \mvee{}  ((s  \mcdot{}  f  j)  =  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  s  \mcdot{}  f  \mmember{}  K  {}\mrightarrow{}  I+j  BY
                          Auto)
  THEN  (RWO  "name-morph-satisfies-comp"  0  THENA  Auto)
  THEN  RWO  "satisfies-face-lattice-tube<"  0
  THEN  Auto)

---

Home Index