---

Step * 1 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
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)))
BY
{ 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)
9. (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)))

2
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)
9. (phi s ⋅ g) = 1 ∨ ((g j) = 0 ∈ Point(dM(K))) ∨ ((g j) = 1 ∈ Point(dM(K)))
⊢ (fl-join(I+j;s(phi);fl-join(I+j;(j=0);(j=1))) g) = 1

---

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
7.  (j=0)  \mmember{}  \mBbbF{}(I+j)
8.  (j=1)  \mmember{}  \mBbbF{}(I+j)
\mvdash{}  (fl-join(I+j;s(phi);fl-join(I+j;(j=0);(j=1)))  g)  =  1
\mLeftarrow{}{}\mRightarrow{}  (phi  s  \mcdot{}  g)  =  1  \mvee{}  ((g  j)  =  0)  \mvee{}  ((g  j)  =  1)


By

---

Latex:
Auto

---

Home Index