---

Step * of Lemma not-not-finite-xmiddle

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

1
1. [T] : Type
2. n : ℕ
3. T ~ ℕn
⊢ ∃f:ℕn ⟶ T. Surj(ℕn;T;f)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `not-not-finite-xmiddle-1`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  UnfoldTopAb  (-1)
  THEN  ParallelLast)

---

Home Index