---

Step * 2 1 3 1 of Lemma combinations-list


1. [A] : Type
2. n : ℕ
3. A ~ ℕn
4. k : ℕ
5. c : ℕ
6. Combination(k;A) ~ ℕc
7. L : Combination(k;A) List
8. no_repeats(Combination(k;A);L)
9. ||L|| = c ∈ ℤ
10. ∀x:Combination(k;A). (x ∈ L)
11. x : A List
12. ||x|| = k ∈ ℤ
13. no_repeats(A;x)
14. (x ∈ L)
⊢ (x ∈ L)
BY
{ xxx(RepeatFor 3 (ParallelLast) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  n  :  \mBbbN{}
3.  A  \msim{}  \mBbbN{}n
4.  k  :  \mBbbN{}
5.  c  :  \mBbbN{}
6.  Combination(k;A)  \msim{}  \mBbbN{}c
7.  L  :  Combination(k;A)  List
8.  no\_repeats(Combination(k;A);L)
9.  ||L||  =  c
10.  \mforall{}x:Combination(k;A).  (x  \mmember{}  L)
11.  x  :  A  List
12.  ||x||  =  k
13.  no\_repeats(A;x)
14.  (x  \mmember{}  L)
\mvdash{}  (x  \mmember{}  L)


By

---

Latex:
xxx(RepeatFor  3  (ParallelLast)  THEN  Auto)xxx

---

Home Index