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


1. Type
2. Type
3. 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. a1 T//t.f[t]
8. a2 T//t.f[t]
9. (f a1) (f a2) ∈ {s:S| ∃t:T. ((f t) s ∈ S)} 
⊢ a1 a2 ∈ T//t.f[t]
BY
(D -3 THEN -2 THEN EqTypeCD THEN Auto) }

1
.....aux..... 
1. Type
2. Type
3. 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. a1 Base
8. a3 Base
9. a1 a3 ∈ pertype(λt,y. ((t ∈ T) ∧ (y ∈ T) ∧ (f[t] f[y] ∈ S)))
10. a1 ∈ T
11. a3 ∈ T
12. f[a1] f[a3] ∈ S
13. a2 Base
14. a4 Base
15. a2 a4 ∈ pertype(λt,y. ((t ∈ T) ∧ (y ∈ T) ∧ (f[t] f[y] ∈ S)))
16. a2 ∈ T
17. a4 ∈ T
18. f[a2] f[a4] ∈ S
19. (f a1) (f a2) ∈ {s:S| ∃t:T. ((f t) s ∈ S)} 
⊢ EquivRel(T;x,y.f[x] f[y] ∈ S)

2
.....antecedent..... 
1. Type
2. Type
3. 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. a1 Base
8. a3 Base
9. a1 a3 ∈ pertype(λt,y. ((t ∈ T) ∧ (y ∈ T) ∧ (f[t] f[y] ∈ S)))
10. a1 ∈ T
11. a3 ∈ T
12. f[a1] f[a3] ∈ S
13. a2 Base
14. a4 Base
15. a2 a4 ∈ pertype(λt,y. ((t ∈ T) ∧ (y ∈ T) ∧ (f[t] f[y] ∈ S)))
16. a2 ∈ T
17. a4 ∈ T
18. f[a2] f[a4] ∈ S
19. (f a1) (f a2) ∈ {s:S| ∃t:T. ((f t) s ∈ S)} 
⊢ f[a1] f[a4] ∈ 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.  a1  :  T//t.f[t]
8.  a2  :  T//t.f[t]
9.  (f  a1)  =  (f  a2)
\mvdash{}  a1  =  a2


By


Latex:
(D  -3  THEN  D  -2  THEN  EqTypeCD  THEN  Auto)




Home Index