---

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


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)))
BY
{ (Unfold `face-lattice-tube` 0
   THEN Fold `fl-join` 0
   THEN (Assert (j=0) ∈ 𝔽(I+j) BY
               (SubsumeC ⌜Point(face_lattice(I+j))⌝⋅ THEN Auto))
   THEN (Assert (j=1) ∈ 𝔽(I+j) BY
               (SubsumeC ⌜Point(face_lattice(I+j))⌝⋅ THEN 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
7. (j=0) ∈ 𝔽(I+j)
8. (j=1) ∈ 𝔽(I+j)
⊢ (fl-join(I+j;s(phi);fl-join(I+j;(j=0);(j=1))) g) = 1
⇐⇒ (phi s ⋅ g) = 1 ∨ ((g j) = 0 ∈ Point(dM(K))) ∨ ((g j) = 1 ∈ Point(dM(K)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  phi  :  \mBbbF{}(I)
4.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\} 
5.  K  :  fset(\mBbbN{})
6.  g  :  K  {}\mrightarrow{}  I+j
\mvdash{}  (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:
(Unfold  `face-lattice-tube`  0
  THEN  Fold  `fl-join`  0
  THEN  (Assert  (j=0)  \mmember{}  \mBbbF{}(I+j)  BY
                          (SubsumeC  \mkleeneopen{}Point(face\_lattice(I+j))\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  (j=1)  \mmember{}  \mBbbF{}(I+j)  BY
                          (SubsumeC  \mkleeneopen{}Point(face\_lattice(I+j))\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index