---

Step * 1 of Lemma equipollent-partition


1. k : ℕ
2. [A] : Type
3. A ~ ℕk
4. [P] : A ⟶ ℙ
5. d : ∀x:A. Dec(P[x])
6. L : A List
7. no_repeats(A;L)
8. ||L|| = k ∈ ℤ
9. ∀x:A. (x ∈ L)
10. ∀x:A. ((isl(d x) ∈ 𝔹) ∧ (↑isl(d x) ⇐⇒ P[x]))
⊢ ∃i,j:ℕ. ((k = (i + j) ∈ ℤ) ∧ {a:A| P[a]}  ~ ℕi ∧ {a:A| ¬P[a]}  ~ ℕj)
BY
{ (InstConcl [⌜||filter(λx.isl(d x);L)||⌝;||filter(λx.(¬bisl(d x));L)||]⋅ THEN Auto) }

1
1. k : ℕ
2. A : Type
3. A ~ ℕk
4. P : A ⟶ ℙ
5. d : ∀x:A. Dec(P[x])
6. L : A List
7. no_repeats(A;L)
8. ||L|| = k ∈ ℤ
9. ∀x:A. (x ∈ L)
10. ∀x:A. ((isl(d x) ∈ 𝔹) ∧ (↑isl(d x) ⇐⇒ P[x]))
⊢ k = (||filter(λx.isl(d x);L)|| + ||filter(λx.(¬bisl(d x));L)||) ∈ ℤ

2
1. k : ℕ
2. [A] : Type
3. A ~ ℕk
4. [P] : A ⟶ ℙ
5. d : ∀x:A. Dec(P[x])
6. L : A List
7. no_repeats(A;L)
8. ||L|| = k ∈ ℤ
9. ∀x:A. (x ∈ L)
10. ∀x:A. ((isl(d x) ∈ 𝔹) ∧ (↑isl(d x) ⇐⇒ P[x]))
11. k = (||filter(λx.isl(d x);L)|| + ||filter(λx.(¬bisl(d x));L)||) ∈ ℤ
⊢ {a:A| P[a]}  ~ ℕ||filter(λx.isl(d x);L)||

3
1. k : ℕ
2. [A] : Type
3. A ~ ℕk
4. [P] : A ⟶ ℙ
5. d : ∀x:A. Dec(P[x])
6. L : A List
7. no_repeats(A;L)
8. ||L|| = k ∈ ℤ
9. ∀x:A. (x ∈ L)
10. ∀x:A. ((isl(d x) ∈ 𝔹) ∧ (↑isl(d x) ⇐⇒ P[x]))
11. k = (||filter(λx.isl(d x);L)|| + ||filter(λx.(¬bisl(d x));L)||) ∈ ℤ
12. {a:A| P[a]}  ~ ℕ||filter(λx.isl(d x);L)||
⊢ {a:A| ¬P[a]}  ~ ℕ||filter(λx.(¬bisl(d x));L)||

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  [A]  :  Type
3.  A  \msim{}  \mBbbN{}k
4.  [P]  :  A  {}\mrightarrow{}  \mBbbP{}
5.  d  :  \mforall{}x:A.  Dec(P[x])
6.  L  :  A  List
7.  no\_repeats(A;L)
8.  ||L||  =  k
9.  \mforall{}x:A.  (x  \mmember{}  L)
10.  \mforall{}x:A.  ((isl(d  x)  \mmember{}  \mBbbB{})  \mwedge{}  (\muparrow{}isl(d  x)  \mLeftarrow{}{}\mRightarrow{}  P[x]))
\mvdash{}  \mexists{}i,j:\mBbbN{}.  ((k  =  (i  +  j))  \mwedge{}  \{a:A|  P[a]\}    \msim{}  \mBbbN{}i  \mwedge{}  \{a:A|  \mneg{}P[a]\}    \msim{}  \mBbbN{}j)


By

---

Latex:
(InstConcl  [\mkleeneopen{}||filter(\mlambda{}x.isl(d  x);L)||\mkleeneclose{};||filter(\mlambda{}x.(\mneg{}\msubb{}isl(d  x));L)||]\mcdot{}  THEN  Auto)

---

Home Index