---

Step * of Lemma s-comp-if-lemma1

∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀x:Point(dM(J)).  (s ⋅ λj.if (j =z new-name(I)) then x else 1 ⋅ f j fi  = f ∈ J ⟶ I)
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN FunExt
   THEN Auto
   THEN RepUR ``nh-comp nc-s nh-id dma-lift-compose`` 0
   THEN Fold `dM` 0
   THEN Fold `dM-lift` 0
   THEN (RWO "dM-lift-inc" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
4. x : Point(dM(J))
5. x1 : names(I)
6. x1 = new-name(I) ∈ ℤ
⊢ x = (f x1) ∈ Point(dM(J))

---

Latex:

---

Latex:
\mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}x:Point(dM(J)).
    (s  \mcdot{}  \mlambda{}j.if  (j  =\msubz{}  new-name(I))  then  x  else  1  \mcdot{}  f  j  fi    =  f)


By

---

Latex:
(Auto
  THEN  Unfold  `names-hom`  0
  THEN  FunExt
  THEN  Auto
  THEN  RepUR  ``nh-comp  nc-s  nh-id  dma-lift-compose``  0
  THEN  Fold  `dM`  0
  THEN  Fold  `dM-lift`  0
  THEN  (RWO  "dM-lift-inc"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index