---

Step * of Lemma nc-e'_wf

∀[I,J:fset(ℕ)]. ∀[i,j:ℕ]. ∀[g:J ⟶ I].  (g,i=j ∈ J+j ⟶ I+i)
BY
{ ((Auto THEN Unfold `nc-e\'` 0) THEN All (Unfold `names-hom`) THEN (FunExt THENA Auto) THEN Reduce 0) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : ℕ
4. j : ℕ
5. g : names(I) ⟶ Point(dM(J))
6. x : names(I+i)
⊢ if (x =z i) then <j> else g x fi  ∈ Point(dM(J+j))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i,j:\mBbbN{}].  \mforall{}[g:J  {}\mrightarrow{}  I].    (g,i=j  \mmember{}  J+j  {}\mrightarrow{}  I+i)


By

---

Latex:
((Auto  THEN  Unfold  `nc-e\mbackslash{}'`  0)  THEN  All  (Unfold  `names-hom`)  THEN  (FunExt  THENA  Auto)  THEN  Reduce  0)

---

Home Index