---

Step * of Lemma s-comp-nc-p

∀[I:fset(ℕ)]. ∀[i:ℕ]. ∀[z:Point(dM(I))].  s ⋅ (i/z) = 1 ∈ I ⟶ I supposing ¬i ∈ I
BY
{ (Auto
   THEN RepUR ``nh-comp nc-s nc-p nh-id names-hom dma-lift-compose`` 0
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN (Fold `dM` 0 THEN Fold `dM-lift` 0)
   THEN (Assert ⌜λx.if (x =z i) then z else <x> fi  ∈ I ⟶ I+i⌝⋅
   THENM ((RWO "dM-lift-inc" 0 THENA Auto) THEN Reduce 0)
   )) }

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

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

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].  \mforall{}[z:Point(dM(I))].    s  \mcdot{}  (i/z)  =  1  supposing  \mneg{}i  \mmember{}  I


By

---

Latex:
(Auto
  THEN  RepUR  ``nh-comp  nc-s  nc-p  nh-id  names-hom  dma-lift-compose``  0
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  (Fold  `dM`  0  THEN  Fold  `dM-lift`  0)
  THEN  (Assert  \mkleeneopen{}\mlambda{}x.if  (x  =\msubz{}  i)  then  z  else  <x>  fi    \mmember{}  I  {}\mrightarrow{}  I+i\mkleeneclose{}\mcdot{}
  THENM  ((RWO  "dM-lift-inc"  0  THENA  Auto)  THEN  Reduce  0)
  ))

---

Home Index