---

Step * 1 1 of Lemma nc-m-nc-1


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. (m(i;j) ⋅ (j1) i) = (j1) i ∧ (j1) j ∈ Point(dM(I+i))
⊢ <i> = if (i =z j) then 1 else <i> fi  ∧ 1 ∈ Point(dM(I+i))
BY
{ AutoSplit }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. (m(i;j) ⋅ (j1) i) = (j1) i ∧ (j1) j ∈ Point(dM(I+i))
5. i = j ∈ ℤ
⊢ <i> = 1 ∧ 1 ∈ Point(dM(I+i))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\} 
4.  (m(i;j)  \mcdot{}  (j1)  i)  =  (j1)  i  \mwedge{}  (j1)  j
\mvdash{}  <i>  =  if  (i  =\msubz{}  j)  then  1  else  <i>  fi    \mwedge{}  1


By

---

Latex:
AutoSplit

---

Home Index