---

Step * of Lemma nh-comp-is-id

∀[I,J:fset(ℕ)].
  ∀[f:I ⟶ J]. ∀[g:J ⟶ I].
    g ⋅ f = 1 ∈ I ⟶ I supposing ∀x:names(I). (((g x) = <x> ∈ Point(dM(J))) ∧ ((f x) = <x> ∈ Point(dM(I)))) 
  supposing I ⊆ J
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN FunExt
   THEN Auto
   THEN RepUR ``nh-id nh-comp dma-lift-compose`` 0
   THEN Fold `dM` 0
   THEN Fold `dM-lift` 0) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. I ⊆ J
4. f : I ⟶ J
5. g : J ⟶ I
6. ∀x:names(I). (((g x) = <x> ∈ Point(dM(J))) ∧ ((f x) = <x> ∈ Point(dM(I))))
7. x : names(I)
⊢ (dM-lift(I;J;f) (g x)) = <x> ∈ Point(dM(I))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].
    \mforall{}[f:I  {}\mrightarrow{}  J].  \mforall{}[g:J  {}\mrightarrow{}  I].    g  \mcdot{}  f  =  1  supposing  \mforall{}x:names(I).  (((g  x)  =  <x>)  \mwedge{}  ((f  x)  =  <x>)) 
    supposing  I  \msubseteq{}  J


By

---

Latex:
(Auto
  THEN  Unfold  `names-hom`  0
  THEN  FunExt
  THEN  Auto
  THEN  RepUR  ``nh-id  nh-comp  dma-lift-compose``  0
  THEN  Fold  `dM`  0
  THEN  Fold  `dM-lift`  0)

---

Home Index