---

Step * of Lemma markov-streamless-function

(∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m))))
⇒ (∀A,B:Type.  ((∃a:ℕ. A ~ ℕa) ⇒ streamless(B) ⇒ streamless(A ⟶ B)))
BY
{ xxx(Auto THEN All (RWO "markov-streamless-iff") THEN Auto)xxx }

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

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

---

Latex:

---

Latex:
(\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))))
{}\mRightarrow{}  (\mforall{}A,B:Type.    ((\mexists{}a:\mBbbN{}.  A  \msim{}  \mBbbN{}a)  {}\mRightarrow{}  streamless(B)  {}\mRightarrow{}  streamless(A  {}\mrightarrow{}  B)))


By

---

Latex:
xxx(Auto  THEN  All  (RWO  "markov-streamless-iff")  THEN  Auto)xxx

---

Home Index