---

Step * 2 1 2 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. L@0 : A List
12. i : ℕ
13. i < ||L||
14. L@0 = L[i] ∈ (A List)
15. v : A List
16. [%22] : no_repeats(A;v) ∧ (||v|| = k ∈ ℤ)
17. L[i] = v ∈ Combination(k;A)
⊢ no_repeats(A;v)
BY
{ (Unhide THEN Auto) }

---

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.  L@0  :  A  List
12.  i  :  \mBbbN{}
13.  i  <  ||L||
14.  L@0  =  L[i]
15.  v  :  A  List
16.  [\%22]  :  no\_repeats(A;v)  \mwedge{}  (||v||  =  k)
17.  L[i]  =  v
\mvdash{}  no\_repeats(A;v)


By

---

Latex:
(Unhide  THEN  Auto)

---

Home Index