---

Step * of Lemma equipollent-partition

No Annotations
∀k:ℕ
  ∀[A:Type]
    (A ~ ℕk
    ⇒ (∀[P:A ⟶ ℙ]. ((∀x:A. Dec(P[x])) ⇒ (∃i,j:ℕ. ((k = (i + j) ∈ ℤ) ∧ {a:A| P[a]}  ~ ℕi ∧ {a:A| ¬P[a]}  ~ ℕj)))))
BY
{ ((UnivCD THENA Auto)
   THEN (FLemma `equipollent-iff-list` [-3] THENA Auto)
   THEN ExRepD
   THEN RenameVar `d' (-5)
   THEN (Assert ∀x:A. ((isl(d x) ∈ 𝔹) ∧ (↑isl(d x) ⇐⇒ P[x])) BY
               ((UnivCD THENA Auto) THEN (GenConclTerm ⌜d x⌝⋅ THENA Auto) THEN D (-2) THEN Reduce 0 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]))
⊢ ∃i,j:ℕ. ((k = (i + j) ∈ ℤ) ∧ {a:A| P[a]}  ~ ℕi ∧ {a:A| ¬P[a]}  ~ ℕj)

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}
    \mforall{}[A:Type]
        (A  \msim{}  \mBbbN{}k
        {}\mRightarrow{}  (\mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}]
                    ((\mforall{}x:A.  Dec(P[x]))  {}\mRightarrow{}  (\mexists{}i,j:\mBbbN{}.  ((k  =  (i  +  j))  \mwedge{}  \{a:A|  P[a]\}    \msim{}  \mBbbN{}i  \mwedge{}  \{a:A|  \mneg{}P[a]\}    \msim{}  \mBbbN{}j))))\000C)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (FLemma  `equipollent-iff-list`  [-3]  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `d'  (-5)
  THEN  (Assert  \mforall{}x:A.  ((isl(d  x)  \mmember{}  \mBbbB{})  \mwedge{}  (\muparrow{}isl(d  x)  \mLeftarrow{}{}\mRightarrow{}  P[x]))  BY
                          ((UnivCD  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}d  x\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  (-2)
                            THEN  Reduce  0
                            THEN  Auto)))

---

Home Index