---

Step * of Lemma finite-product

No Annotations
∀[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:
No  Annotations
\mforall{}[S:Type].  \mforall{}[T:S  {}\mrightarrow{}  Type].    (finite(S)  {}\mRightarrow{}  (\mforall{}s:S.  finite(T[s]))  {}\mRightarrow{}  finite(s:S  \mtimes{}  T[s]))


By

---

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

---

Home Index