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