---

Step * of Lemma satisfies-face-lattice-tube

∀I:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀phi:𝔽(I). ∀j:{j:ℕ| ¬j ∈ I+i} . ∀K:fset(ℕ). ∀g:K ⟶ I+j.
  ((face-lattice-tube(I;phi;j) g) = 1 ⇐⇒ (phi s ⋅ g) = 1 ∨ ((g j) = 0 ∈ Point(dM(K))) ∨ ((g j) = 1 ∈ Point(dM(K))))
BY
{ (UnivCD THENA Auto) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. phi : 𝔽(I)
4. j : {j:ℕ| ¬j ∈ I+i} 
5. K : fset(ℕ)
6. g : K ⟶ I+j
⊢ (face-lattice-tube(I;phi;j) g) = 1 ⇐⇒ (phi s ⋅ g) = 1 ∨ ((g j) = 0 ∈ Point(dM(K))) ∨ ((g j) = 1 ∈ Point(dM(K)))

---

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{}g:K  {}\mrightarrow{}  I+j.
    ((face-lattice-tube(I;phi;j)  g)  =  1  \mLeftarrow{}{}\mRightarrow{}  (phi  s  \mcdot{}  g)  =  1  \mvee{}  ((g  j)  =  0)  \mvee{}  ((g  j)  =  1))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index