Step * 2 of Lemma finite-iff-listable


1. [T] Type
2. ∃L:T List. (no_repeats(T;L) ∧ (∀x:T. (x ∈ L)))
⊢ finite(T)
BY
(ExRepD THEN With ⌜||L||⌝  THEN Auto) }

1
1. [T] Type
2. List
3. no_repeats(T;L)
4. ∀x:T. (x ∈ L)
⊢ ~ ℕ||L||


Latex:


Latex:

1.  [T]  :  Type
2.  \mexists{}L:T  List.  (no\_repeats(T;L)  \mwedge{}  (\mforall{}x:T.  (x  \mmember{}  L)))
\mvdash{}  finite(T)


By


Latex:
(ExRepD  THEN  D  0  With  \mkleeneopen{}||L||\mkleeneclose{}    THEN  Auto)




Home Index