---

Step * of Lemma not-l_all-dec

∀[T:Type]. ∀L:T List. ∀P:T ⟶ ℙ.  ((∀x:T. Dec(P[x])) ⇒ (¬(∀x∈L.P[x]) ⇐⇒ (∃x∈L. ¬P[x])))
BY
{ Auto }

1
1. [T] : Type
2. L : T List@i
3. P : T ⟶ ℙ@i'
4. ∀x:T. Dec(P[x])@i
5. ¬(∀x∈L.P[x])@i
⊢ (∃x∈L. ¬P[x])

2
1. T : Type
2. L : T List@i
3. P : T ⟶ ℙ@i'
4. ∀x:T. Dec(P[x])@i
5. (∃x∈L. ¬P[x])@i
⊢ ¬(∀x∈L.P[x])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.    ((\mforall{}x:T.  Dec(P[x]))  {}\mRightarrow{}  (\mneg{}(\mforall{}x\mmember{}L.P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}x\mmember{}L.  \mneg{}P[x])))


By

---

Latex:
Auto

---

Home Index