---

Step * 1 1 of Lemma free-iso-int_wf

.....assertion..... 
1. S : Type
2. s : S
3. ∀x,y:S.  (x = y ∈ S)
4. free-1-iso(s;ℤ-rng) ∈ free-vs(ℤ-rng;S) ≅ ℤ
⊢ free-1-iso(s;ℤ-rng) = free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ
BY
{ All (RepUR ``vs-iso free-1-iso free-iso-int exists``) }

1
1. S : Type
2. s : S
3. ∀x,y:S.  (x = y ∈ S)
4. <λx.Σ(p∈x). let k,s = p in k * 1, λk.{<k * 1, s>}, λb.Ax, λa.Ax> ∈ f:free-vs(ℤ-rng;S) ⟶ ℤ
   × g:ℤ ⟶ free-vs(ℤ-rng;S)
   × ((∀a:Point(free-vs(ℤ-rng;S)). ((g (f a)) = a ∈ Point(free-vs(ℤ-rng;S))))
     ∧ (∀b:Point(ℤ). ((f (g b)) = b ∈ Point(ℤ))))
⊢ <λx.Σ(p∈x). let k,s = p in k * 1, λk.{<k * 1, s>}, λb.Ax, λa.Ax>
= <λx.Σ(p∈x). let k,s = p in k, λk.{<k, s>}, λb.Ax, λa.Ax>
∈ (f:free-vs(ℤ-rng;S) ⟶ ℤ
  × g:ℤ ⟶ free-vs(ℤ-rng;S)
  × ((∀a:Point(free-vs(ℤ-rng;S)). ((g (f a)) = a ∈ Point(free-vs(ℤ-rng;S))))
    ∧ (∀b:Point(ℤ). ((f (g b)) = b ∈ Point(ℤ)))))

---

Latex:

---

Latex:
.....assertion..... 
1.  S  :  Type
2.  s  :  S
3.  \mforall{}x,y:S.    (x  =  y)
4.  free-1-iso(s;\mBbbZ{}-rng)  \mmember{}  free-vs(\mBbbZ{}-rng;S)  \mcong{}  \mBbbZ{}
\mvdash{}  free-1-iso(s;\mBbbZ{}-rng)  =  free-iso-int(s)


By

---

Latex:
All  (RepUR  ``vs-iso  free-1-iso  free-iso-int  exists``)

---

Home Index