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