---

Step * of Lemma not-assert-bdd-all

∀n:ℕ. ∀P:ℕn ⟶ 𝔹.  (¬↑bdd-all(n;i.P[i]) ⇐⇒ ∃i:ℕn. (¬↑P[i]))
BY
{ (RWO "assert-bdd-all" 0 THEN Auto) }

1
1. n : ℕ
2. P : ℕn ⟶ 𝔹
3. ¬(∀i:ℕn. (↑P[i]))
⊢ ∃i:ℕn. (¬↑P[i])

2
1. n : ℕ
2. P : ℕn ⟶ 𝔹
3. ∃i:ℕn. (¬↑P[i])
⊢ ¬(∀i:ℕn. (↑P[i]))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}P:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    (\mneg{}\muparrow{}bdd-all(n;i.P[i])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (\mneg{}\muparrow{}P[i]))


By

---

Latex:
(RWO  "assert-bdd-all"  0  THEN  Auto)

---

Home Index