---

Step * of Lemma equipollent-split

No Annotations
∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Dec(↓P[x])) ⇒ T ~ {x:T| P[x]}  + {x:T| ¬P[x]} )
BY
{ (Auto THEN RWO "equipollent-set" 0 THEN Auto) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(↓P[x])
⊢ T ~ {x:T| ↓P[x]}  + {x:T| ↓¬P[x]} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  Dec(\mdownarrow{}P[x]))  {}\mRightarrow{}  T  \msim{}  \{x:T|  P[x]\}    +  \{x:T|  \mneg{}P[x]\}  )


By

---

Latex:
(Auto  THEN  RWO  "equipollent-set"  0  THEN  Auto)

---

Home Index