Step
*
of Lemma
equipollent-subtract
∀a,b:ℕ. ∀[P:ℕa ⟶ ℙ]. ({x:ℕa| P[x]} ~ ℕb
⇒ {x:ℕa| ¬P[x]} ~ ℕa - b)
BY
{ xxx(Auto THEN FLemma `equipollent_inversion` [-1] THEN Auto)xxx }
1
1. a : ℕ
2. b : ℕ
3. [P] : ℕa ⟶ ℙ
4. {x:ℕa| P[x]} ~ ℕb
5. ℕb ~ {x:ℕa| P[x]}
⊢ {x:ℕa| ¬P[x]} ~ ℕa - b
Latex:
Latex:
\mforall{}a,b:\mBbbN{}. \mforall{}[P:\mBbbN{}a {}\mrightarrow{} \mBbbP{}]. (\{x:\mBbbN{}a| P[x]\} \msim{} \mBbbN{}b {}\mRightarrow{} \{x:\mBbbN{}a| \mneg{}P[x]\} \msim{} \mBbbN{}a - b)
By
Latex:
xxx(Auto THEN FLemma `equipollent\_inversion` [-1] THEN Auto)xxx
Home
Index