---

Step * of Lemma equipollent-nat-subset

∀[T:Type]. ∀P:T ⟶ ℙ. ((∀x:T. Dec(P[x])) ⇒ (∀L:T List. ∃x:T. (P[x] ∧ (¬(x ∈ L)))) ⇒ ℕ ~ T ⇒ ℕ ~ {x:T| P[x]} )
BY
{ (Auto THEN D -1 THEN (InstLemma `equipollent-nat-decidable-subset` [⌜λ2n.P[f n]⌝]⋅ THENA Auto)) }

1
1. [T] : Type
2. P : T ⟶ ℙ@i'
3. ∀x:T. Dec(P[x])@i
4. ∀L:T List. ∃x:T. (P[x] ∧ (¬(x ∈ L)))@i
5. f : ℕ ⟶ T@i
6. Bij(ℕ;T;f)@i
7. m : ℕ@i
⊢ ∃n:ℕ. (P[f n] ∧ (m ≤ n))

2
1. [T] : Type
2. P : T ⟶ ℙ@i'
3. ∀x:T. Dec(P[x])@i
4. ∀L:T List. ∃x:T. (P[x] ∧ (¬(x ∈ L)))@i
5. f : ℕ ⟶ T@i
6. Bij(ℕ;T;f)@i
7. ℕ ~ {n:ℕ| P[f n]} 
⊢ ℕ ~ {x:T| P[x]} 

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}
        ((\mforall{}x:T.  Dec(P[x]))  {}\mRightarrow{}  (\mforall{}L:T  List.  \mexists{}x:T.  (P[x]  \mwedge{}  (\mneg{}(x  \mmember{}  L))))  {}\mRightarrow{}  \mBbbN{}  \msim{}  T  {}\mRightarrow{}  \mBbbN{}  \msim{}  \{x:T|  P[x]\}  )


By

---

Latex:
(Auto  THEN  D  -1  THEN  (InstLemma  `equipollent-nat-decidable-subset`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.P[f  n]\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index