---

Step * 1 of Lemma finite-type-iff-list


1. [T] : Type
2. finite-type(T)@i
⊢ ∃L:T List. ∀x:T. (x ∈ L)
BY
{ (D -1 THEN ((InstLemma `cardinality-le-list` [⌜T⌝; ⌜n⌝])⋅ THENA Auto)) }

1
1. [T] : Type
2. n : ℕ@i
3. ∃f:ℕn ⟶ T. Surj(ℕn;T;f)@i
4. ∃L:T List. ((||L|| = n ∈ ℤ) ∧ (∀x:T. (x ∈ L)))
⊢ ∃L:T List. ∀x:T. (x ∈ L)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  finite-type(T)@i
\mvdash{}  \mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L)


By

---

Latex:
(D  -1  THEN  ((InstLemma  `cardinality-le-list`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index