---

Step * of Lemma dM-lift-is-id2

∀[I:fset(ℕ)]. ∀[J,K:{K:fset(ℕ)| I ⊆ K} ]. ∀[h:K ⟶ J].
  ∀[x:Point(dM(I))]. ((dM-lift(K;J;h) x) = x ∈ Point(dM(K))) supposing ∀i:names(I). ((h i) = <i> ∈ Point(dM(K)))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `compose-dma-hom` [⌜dM(I)⌝;⌜dM(J)⌝;⌜dM(K)⌝;⌜λv.v⌝;⌜dM-lift(K;J;h)⌝]⋅
         THENA (Try (BLemma `dM-subobject`) THEN Auto)
         )
   THEN (InstLemma `dM-dM-homs-equal` [⌜I⌝;⌜K⌝;⌜dM-lift(K;J;h) o (λv.v)⌝;⌜λv.v⌝]⋅
         THENA (Try (BLemma `dM-subobject`) THEN Auto)
         )) }

1
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. K : {K:fset(ℕ)| I ⊆ K} 
4. h : K ⟶ J
5. ∀i:names(I). ((h i) = <i> ∈ Point(dM(K)))
6. x : Point(dM(I))
7. dM-lift(K;J;h) o (λv.v) ∈ dma-hom(dM(I);dM(K))
8. (dM-lift(K;J;h) o (λv.v)) = (λv.v) ∈ (Point(dM(I)) ⟶ Point(dM(K)))
⊢ (dM-lift(K;J;h) x) = x ∈ Point(dM(K))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[J,K:\{K:fset(\mBbbN{})|  I  \msubseteq{}  K\}  ].  \mforall{}[h:K  {}\mrightarrow{}  J].
    \mforall{}[x:Point(dM(I))].  ((dM-lift(K;J;h)  x)  =  x)  supposing  \mforall{}i:names(I).  ((h  i)  =  <i>)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `compose-dma-hom`  [\mkleeneopen{}dM(I)\mkleeneclose{};\mkleeneopen{}dM(J)\mkleeneclose{};\mkleeneopen{}dM(K)\mkleeneclose{};\mkleeneopen{}\mlambda{}v.v\mkleeneclose{};\mkleeneopen{}dM-lift(K;J;h)\mkleeneclose{}]\mcdot{}
              THENA  (Try  (BLemma  `dM-subobject`)  THEN  Auto)
              )
  THEN  (InstLemma  `dM-dM-homs-equal`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}dM-lift(K;J;h)  o  (\mlambda{}v.v)\mkleeneclose{};\mkleeneopen{}\mlambda{}v.v\mkleeneclose{}]\mcdot{}
              THENA  (Try  (BLemma  `dM-subobject`)  THEN  Auto)
              ))

---

Home Index