---

Step * of Lemma nh-id-right

∀I,J:fset(ℕ). ∀f:I ⟶ J.  (1 ⋅ f = f ∈ I ⟶ J)
BY
{ (Auto
   THEN RepUR ``nh-comp nh-id names-hom dma-lift-compose dM_inc`` 0
   THEN (FunExt THENA Auto)
   THEN Unfold `names-hom` -2
   THEN (GenConclTerm 
         ⌜free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);free-dml-deq(names(I);NamesDeq);f)⌝⋅
         THENA (Auto THEN RWO "free-dma-point" 0 THEN Auto)
         )) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : names(J) ⟶ Point(dM(I))
4. x : names(J)
5. v : {g:dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);free-DeMorgan-algebra(names(I);NamesDeq))| 
        ∀i:names(J). ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(names(I);NamesDeq)))} 
6. free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);free-dml-deq(names(I);NamesDeq);f)
= v
∈ {g:dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);free-DeMorgan-algebra(names(I);NamesDeq))| 
   ∀i:names(J). ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(names(I);NamesDeq)))} 
⊢ ((v o (λx.<x>)) x) = (f x) ∈ Point(dM(I))

---

Latex:

---

Latex:
\mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:I  {}\mrightarrow{}  J.    (1  \mcdot{}  f  =  f)


By

---

Latex:
(Auto
  THEN  RepUR  ``nh-comp  nh-id  names-hom  dma-lift-compose  dM\_inc``  0
  THEN  (FunExt  THENA  Auto)
  THEN  Unfold  `names-hom`  -2
  THEN  (GenConclTerm 
              \mkleeneopen{}free-dma-lift(names(J);NamesDeq;free-DeMorgan-algebra(names(I);NamesDeq);...;f)\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  RWO  "free-dma-point"  0  THEN  Auto)
              ))

---

Home Index