---

Step * of Lemma combinations-list

∀[A:Type]. ∀n:ℕ. (A ~ ℕn ⇒ (∀k:ℕ. ∃C:A List List. ∀L:A List. ((L ∈ C) ⇐⇒ (||L|| = k ∈ ℤ) ∧ no_repeats(A;L))))
BY
{ xxx(Auto THEN Assert ⌜∃c:ℕ. Combination(k;A) ~ ℕc⌝⋅)xxx }

1
.....assertion..... 
1. [A] : Type
2. n : ℕ
3. A ~ ℕn
4. k : ℕ
⊢ ∃c:ℕ. Combination(k;A) ~ ℕc

2
1. [A] : Type
2. n : ℕ
3. A ~ ℕn
4. k : ℕ
5. ∃c:ℕ. Combination(k;A) ~ ℕc
⊢ ∃C:A List List. ∀L:A List. ((L ∈ C) ⇐⇒ (||L|| = k ∈ ℤ) ∧ no_repeats(A;L))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}n:\mBbbN{}.  (A  \msim{}  \mBbbN{}n  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}.  \mexists{}C:A  List  List.  \mforall{}L:A  List.  ((L  \mmember{}  C)  \mLeftarrow{}{}\mRightarrow{}  (||L||  =  k)  \mwedge{}  no\_repeats(A;L))))


By

---

Latex:
xxx(Auto  THEN  Assert  \mkleeneopen{}\mexists{}c:\mBbbN{}.  Combination(k;A)  \msim{}  \mBbbN{}c\mkleeneclose{}\mcdot{})xxx

---

Home Index