---

Step * of Lemma not-all-finite

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Dec(P[x])) ⇒ (∃k:ℕ. T ~ ℕk) ⇒ (¬(∀x:T. P[x]) ⇐⇒ ∃x:T. (¬P[x])))
BY
{ (Auto THEN Try (((D 0 THENA Auto) THEN ExRepD THEN D -2 THEN Auto)) THEN ExRepD) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. T ~ ℕk
6. ¬(∀x:T. P[x])
⊢ ∃x:T. (¬P[x])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  Dec(P[x]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  (\mneg{}(\mforall{}x:T.  P[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:T.  (\mneg{}P[x])))


By

---

Latex:
(Auto  THEN  Try  (((D  0  THENA  Auto)  THEN  ExRepD  THEN  D  -2  THEN  Auto))  THEN  ExRepD)

---

Home Index