---

Step * of Lemma not-not-finite-xmiddle-1

No Annotations
∀[T:Type]. ((∃n:ℕ. ∃f:ℕn ⟶ T. Surj(ℕn;T;f)) ⇒ (∀P:T ⟶ ℙ. (¬¬(∀i:T. (P[i] ∨ (¬P[i]))))))
BY
{ (Auto
   THEN ExRepD
   THEN (InstLemma `not-not-all-int_seg-xmiddle` [⌜0⌝;⌜n⌝;⌜λ2i.P[f i]⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (D 0 THENA Auto)
   THEN (D 4 With ⌜i⌝  THENA Auto)) }

1
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. P : T ⟶ ℙ
5. ∀i:ℕn. (P[f i] ∨ (¬P[f i]))
6. i : T
7. ∃a:ℕn. ((f a) = i ∈ T)
⊢ P[i] ∨ (¬P[i])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  ((\mexists{}n:\mBbbN{}.  \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  T.  Surj(\mBbbN{}n;T;f))  {}\mRightarrow{}  (\mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  (\mneg{}\mneg{}(\mforall{}i:T.  (P[i]  \mvee{}  (\mneg{}P[i]))))))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (InstLemma  `not-not-all-int\_seg-xmiddle`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.P[f  i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  0  THENA  Auto)
  THEN  (D  4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto))

---

Home Index