---

Step * 1 of Lemma finite-injective-quotient

.....assertion..... 
1. T : Type
2. S : Type
3. f : T ⟶ S
4. finite(S)
5. ∀s:S. Dec(∃t:T. (f[t] = s ∈ S))
⊢ T//t.f[t] ~ {s:S| ∃t:T. ((f t) = s ∈ S)} 
BY
{ (Assert f ∈ T//t.f[t] ⟶ {s:S| ∃t:T. ((f t) = s ∈ S)}  BY
         ((FunExt THENW Auto) THEN D -1 THEN EqTypeCD THEN Auto THEN D 0 With ⌜x⌝  THEN Auto)) }

1
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)} 
⊢ T//t.f[t] ~ {s:S| ∃t:T. ((f t) = s ∈ S)} 

---

Latex:

---

Latex:
.....assertion..... 
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))
\mvdash{}  T//t.f[t]  \msim{}  \{s:S|  \mexists{}t:T.  ((f  t)  =  s)\} 


By

---

Latex:
(Assert  f  \mmember{}  T//t.f[t]  {}\mrightarrow{}  \{s:S|  \mexists{}t:T.  ((f  t)  =  s)\}    BY
              ((FunExt  THENW  Auto)  THEN  D  -1  THEN  EqTypeCD  THEN  Auto  THEN  D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto))

---

Home Index