---

Step * 1 of Lemma DNS-iff-not-not-GMP


1. A : ℕ ⟶ ℙ
2. DNSi.A[i]@i
⊢ ¬¬GMPi.A[i])
BY
{ (Unfold `generalized-markov-principle` 0 THEN Unfold `double-negation-shift` (-1)) }

1
1. A : ℕ ⟶ ℙ
2. (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))@i
⊢ ¬¬((¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n])))

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  DNSi.A[i]@i
\mvdash{}  \mneg{}\mneg{}GMPi.A[i])


By

---

Latex:
(Unfold  `generalized-markov-principle`  0  THEN  Unfold  `double-negation-shift`  (-1))

---

Home Index