---

Step * 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. (no_repeats(Combination(k;A);L) ∧ (||L|| = c ∈ ℤ) ∧ (∀x:Combination(k;A). (x ∈ L)))
⊢ ∃C:A List List. ∀L:A List. ((L ∈ C) ⇐⇒ (||L|| = k ∈ ℤ) ∧ no_repeats(A;L))
BY
{ xxx(ParallelLast THEN Auto)xxx }

1
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. (L@0 ∈ L)
⊢ ||L@0|| = k ∈ ℤ

2
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. (L@0 ∈ L)
⊢ no_repeats(A;L@0)

3
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. ||L@0|| = k ∈ ℤ
13. no_repeats(A;L@0)
⊢ (L@0 ∈ L)

---

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.  \mexists{}L:Combination(k;A)  List
        (no\_repeats(Combination(k;A);L)  \mwedge{}  (||L||  =  c)  \mwedge{}  (\mforall{}x:Combination(k;A).  (x  \mmember{}  L)))
\mvdash{}  \mexists{}C:A  List  List.  \mforall{}L:A  List.  ((L  \mmember{}  C)  \mLeftarrow{}{}\mRightarrow{}  (||L||  =  k)  \mwedge{}  no\_repeats(A;L))


By

---

Latex:
xxx(ParallelLast  THEN  Auto)xxx

---

Home Index