---

Step * of Lemma classical-markov

∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) ⇒ (¬(∀n:ℕ. (¬P[n]))) ⇒ (∃n:ℕ. P[n]))
BY
{ (Auto THEN Assert ⌜{∃n:ℕ. P[n]}⌝⋅) }

1
.....assertion..... 
1. P : ℕ ⟶ ℙ@i'
2. ∀n:ℕ. Dec(P[n])@i
3. ¬(∀n:ℕ. (¬P[n]))@i
⊢ {∃n:ℕ. P[n]}

2
1. P : ℕ ⟶ ℙ@i'
2. ∀n:ℕ. Dec(P[n])@i
3. ¬(∀n:ℕ. (¬P[n]))@i
4. {∃n:ℕ. P[n]}
⊢ ∃n:ℕ. P[n]

---

Latex:

---

Latex:
\mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}n:\mBbbN{}.  Dec(P[n]))  {}\mRightarrow{}  (\mneg{}(\mforall{}n:\mBbbN{}.  (\mneg{}P[n])))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  P[n]))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\{\mexists{}n:\mBbbN{}.  P[n]\}\mkleeneclose{}\mcdot{})

---

Home Index