---

Step * 1 1 1 2 1 of Lemma finite-injective-quotient


1. T : Type
2. S : Type
3. f : T ⟶ S
4. finite(S)
5. ∀s:S. Dec(∃t:T. (f[t] = s ∈ S))
6. {f ∈ T//t.f[t] ⟶ {s:S| ∃t:T. ((f t) = s ∈ S)} }
7. b : {s:S| ∃t:T. ((f t) = s ∈ S)} 
8. t : T
9. (f t) = b ∈ S
⊢ ∃a:T//t.f[t]. ((f a) = b ∈ {s:S| ∃t:T. ((f t) = s ∈ S)} )
BY
{ D 0 With ⌜t⌝  }

1
.....wf..... 
1. T : Type
2. S : Type
3. f : T ⟶ S
4. finite(S)
5. ∀s:S. Dec(∃t:T. (f[t] = s ∈ S))
6. {f ∈ T//t.f[t] ⟶ {s:S| ∃t:T. ((f t) = s ∈ S)} }
7. b : {s:S| ∃t:T. ((f t) = s ∈ S)} 
8. t : T
9. (f t) = b ∈ S
⊢ t ∈ T//t.f[t]

2
1. T : Type
2. S : Type
3. f : T ⟶ S
4. finite(S)
5. ∀s:S. Dec(∃t:T. (f[t] = s ∈ S))
6. {f ∈ T//t.f[t] ⟶ {s:S| ∃t:T. ((f t) = s ∈ S)} }
7. b : {s:S| ∃t:T. ((f t) = s ∈ S)} 
8. t : T
9. (f t) = b ∈ S
⊢ (f t) = b ∈ {s:S| ∃t:T. ((f t) = s ∈ S)} 

3
.....wf..... 
1. T : Type
2. S : Type
3. f : T ⟶ S
4. finite(S)
5. ∀s:S. Dec(∃t:T. (f[t] = s ∈ S))
6. {f ∈ T//t.f[t] ⟶ {s:S| ∃t:T. ((f t) = s ∈ S)} }
7. b : {s:S| ∃t:T. ((f t) = s ∈ S)} 
8. t : T
9. (f t) = b ∈ S
10. a : T//t.f[t]
⊢ istype((f a) = b ∈ {s:S| ∃t:T. ((f t) = s ∈ S)} )

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  f  :  T  {}\mrightarrow{}  S
4.  finite(S)
5.  \mforall{}s:S.  Dec(\mexists{}t:T.  (f[t]  =  s))
6.  \{f  \mmember{}  T//t.f[t]  {}\mrightarrow{}  \{s:S|  \mexists{}t:T.  ((f  t)  =  s)\}  \}
7.  b  :  \{s:S|  \mexists{}t:T.  ((f  t)  =  s)\} 
8.  t  :  T
9.  (f  t)  =  b
\mvdash{}  \mexists{}a:T//t.f[t].  ((f  a)  =  b)


By

---

Latex:
D  0  With  \mkleeneopen{}t\mkleeneclose{} 

---

Home Index