---

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


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]))
BY
{ ((Assert ℕn ~ T BY EAuto 1) THEN D -1) }

1
1. T : Type
2. n : ℕ
3. T ~ ℕn
4. P : T ⟶ ℙ
5. ∀i:T. (P[i] ∨ (¬P[i]))
6. f : ℕn ⟶ T
7. Bij(ℕn;T;f)
⊢ (∃i:T. P[i]) ∨ (∀i: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]))
\mvdash{}  (\mexists{}i:T.  P[i])  \mvee{}  (\mforall{}i:T.  (\mneg{}P[i]))


By

---

Latex:
((Assert  \mBbbN{}n  \msim{}  T  BY  EAuto  1)  THEN  D  -1)

---

Home Index