---

Step * of Lemma finite-injective-quotient

∀T,S:Type. ∀f:T ⟶ S.  (finite(S) ⇒ (∀s:S. Dec(∃t:T. (f[t] = s ∈ S))) ⇒ finite(T//t.f[t]))
BY
{ (Auto THEN Assert ⌜T//t.f[t] ~ {s:S| ∃t:T. ((f t) = s ∈ S)} ⌝⋅) }

1
.....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)} 

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

---

Latex:

---

Latex:
\mforall{}T,S:Type.  \mforall{}f:T  {}\mrightarrow{}  S.    (finite(S)  {}\mRightarrow{}  (\mforall{}s:S.  Dec(\mexists{}t:T.  (f[t]  =  s)))  {}\mRightarrow{}  finite(T//t.f[t]))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}T//t.f[t]  \msim{}  \{s:S|  \mexists{}t:T.  ((f  t)  =  s)\}  \mkleeneclose{}\mcdot{})

---

Home Index