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


1. Type
2. : ℕ
3. ~ ℕn
4. T ⟶ ℙ
5. ∀i:T. (P[i] ∨ P[i]))
6. : ℕn ⟶ T
7. Bij(ℕn;T;f)
⊢ (∀i:T. P[i]) ∨ (∃i:T. P[i]))
BY
(Fold `decidable` (-3)
   THEN (Assert ∀i:ℕn. Dec(P[f i]) BY
               Auto)
   THEN (Assert Dec(∃i:ℕn. P[f i])) BY
               Auto)
   THEN Unfold `decidable` -1
   THEN (D -1 THENL [OrRight; OrLeft])
   THEN Auto) }

1
1. Type
2. : ℕ
3. ~ ℕn
4. T ⟶ ℙ
5. ∀i:T. Dec(P[i])
6. : ℕn ⟶ T
7. Bij(ℕn;T;f)
8. ∀i:ℕn. Dec(P[f i])
9. ∃i:ℕn. P[f i])
⊢ ∃i:T. P[i])

2
1. Type
2. : ℕ
3. ~ ℕn
4. T ⟶ ℙ
5. ∀i:T. Dec(P[i])
6. : ℕn ⟶ T
7. Bij(ℕn;T;f)
8. ∀i:ℕn. Dec(P[f i])
9. ¬(∃i:ℕn. P[f i]))
10. T
⊢ P[i]


Latex:


Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  T  \msim{}  \mBbbN{}n
4.  P  :  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}i:T.  (P[i]  \mvee{}  (\mneg{}P[i]))
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  Bij(\mBbbN{}n;T;f)
\mvdash{}  (\mforall{}i:T.  P[i])  \mvee{}  (\mexists{}i:T.  (\mneg{}P[i]))


By


Latex:
(Fold  `decidable`  (-3)
  THEN  (Assert  \mforall{}i:\mBbbN{}n.  Dec(P[f  i])  BY
                          Auto)
  THEN  (Assert  Dec(\mexists{}i:\mBbbN{}n.  (\mneg{}P[f  i]))  BY
                          Auto)
  THEN  Unfold  `decidable`  -1
  THEN  (D  -1  THENL  [OrRight;  OrLeft])
  THEN  Auto)




Home Index