---

Step * 1 of Lemma markov-streamless-product


1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m)))
2. A : Type
3. B : Type
4. ∀x,y:A.  Dec(x = y ∈ A)
5. ¬¬(∃n:ℕ. A ~ ℕn)
6. ∀x,y:B.  Dec(x = y ∈ B)
7. ¬¬(∃n:ℕ. B ~ ℕn)
8. ∀x,y:A × B.  Dec(x = y ∈ (A × B))
⊢ ¬¬(∃n:ℕ. A × B ~ ℕn)
BY
{ TACTIC:((D 0 THENA Auto) THEN (D -3 THEN (D 0 THENA Auto)) THEN D -5 THEN (D 0 THENA Auto) THEN D -3) }

1
1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m)))
2. A : Type
3. B : Type
4. ∀x,y:A.  Dec(x = y ∈ A)
5. ∀x,y:B.  Dec(x = y ∈ B)
6. ∀x,y:A × B.  Dec(x = y ∈ (A × B))
7. ∃n:ℕ. B ~ ℕn
8. ∃n:ℕ. A ~ ℕn
⊢ ∃n:ℕ. A × B ~ ℕn

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}m:\mBbbN{}.  ((P  m)  \mvee{}  (\mneg{}(P  m))))  {}\mRightarrow{}  (\mneg{}(\mforall{}m:\mBbbN{}.  (\mneg{}(P  m))))  {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  (P  m)))
2.  A  :  Type
3.  B  :  Type
4.  \mforall{}x,y:A.    Dec(x  =  y)
5.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  A  \msim{}  \mBbbN{}n)
6.  \mforall{}x,y:B.    Dec(x  =  y)
7.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  B  \msim{}  \mBbbN{}n)
8.  \mforall{}x,y:A  \mtimes{}  B.    Dec(x  =  y)
\mvdash{}  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  A  \mtimes{}  B  \msim{}  \mBbbN{}n)


By

---

Latex:
TACTIC:((D  0  THENA  Auto)
                THEN  (D  -3  THEN  (D  0  THENA  Auto))
                THEN  D  -5
                THEN  (D  0  THENA  Auto)
                THEN  D  -3)

---

Home Index