---

Step * of Lemma not-not-finite-exists-or-all

No Annotations
∀[T:Type]. (finite(T) ⇒ (∀P:T ⟶ ℙ. (¬¬((∃i:T. P[i]) ∨ (∀i:T. (¬P[i]))))))
BY
{ (InstLemma `not-not-finite-xmiddle` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto)) THEN D 2) }

1
1. T : Type
2. n : ℕ
3. T ~ ℕn
4. P : T ⟶ ℙ
5. ∀i:T. (P[i] ∨ (¬P[i]))
⊢ (∃i:T. P[i]) ∨ (∀i:T. (¬P[i]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  (finite(T)  {}\mRightarrow{}  (\mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  (\mneg{}\mneg{}((\mexists{}i:T.  P[i])  \mvee{}  (\mforall{}i:T.  (\mneg{}P[i]))))))


By

---

Latex:
(InstLemma  `not-not-finite-xmiddle`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))  THEN  D  2)

---

Home Index