---

Step * of Lemma finite-function

∀S:Type. ∀T:S ⟶ Type.  (finite(S) ⇒ (∀s:S. finite(T[s])) ⇒ finite(s:S ⟶ T[s]))
BY
{ (Auto THEN All (Unfold `finite`)⋅ THEN ExRepD THEN (Skolemize (-1) `f'  THENA Auto)) }

1
1. S : Type
2. T : S ⟶ Type
3. n : ℕ
4. S ~ ℕn
5. ∀s:S. ∃n:ℕ. T[s] ~ ℕn
6. f : s:S ⟶ ℕ
7. ∀s:S. T[s] ~ ℕf s
⊢ ∃n:ℕ. s:S ⟶ T[s] ~ ℕn

---

Latex:

---

Latex:
\mforall{}S:Type.  \mforall{}T:S  {}\mrightarrow{}  Type.    (finite(S)  {}\mRightarrow{}  (\mforall{}s:S.  finite(T[s]))  {}\mRightarrow{}  finite(s:S  {}\mrightarrow{}  T[s]))


By

---

Latex:
(Auto  THEN  All  (Unfold  `finite`)\mcdot{}  THEN  ExRepD  THEN  (Skolemize  (-1)  `f'    THENA  Auto))

---

Home Index