---

Step * 1 1 1 1 1 of Lemma markov-streamless-function


1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m)))
2. A : Type
3. B : Type
4. a : ℕ
5. A ~ ℕa
6. ∀x,y:B.  Dec(x = y ∈ B)
7. ¬¬(∃n:ℕ. B ~ ℕn)
8. x : A ⟶ B
9. y : A ⟶ B
10. f : ℕa ⟶ A
11. Bij(ℕa;A;f)
12. ∀i:ℕa. ((x (f i)) = (y (f i)) ∈ B)
13. aa : A
⊢ (x aa) = (y aa) ∈ B
BY
{ xxxD -3xxx }

1
1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m)))
2. A : Type
3. B : Type
4. a : ℕ
5. A ~ ℕa
6. ∀x,y:B.  Dec(x = y ∈ B)
7. ¬¬(∃n:ℕ. B ~ ℕn)
8. x : A ⟶ B
9. y : A ⟶ B
10. f : ℕa ⟶ A
11. Inj(ℕa;A;f)
12. Surj(ℕa;A;f)
13. ∀i:ℕa. ((x (f i)) = (y (f i)) ∈ B)
14. aa : A
⊢ (x aa) = (y aa) ∈ B

---

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.  a  :  \mBbbN{}
5.  A  \msim{}  \mBbbN{}a
6.  \mforall{}x,y:B.    Dec(x  =  y)
7.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  B  \msim{}  \mBbbN{}n)
8.  x  :  A  {}\mrightarrow{}  B
9.  y  :  A  {}\mrightarrow{}  B
10.  f  :  \mBbbN{}a  {}\mrightarrow{}  A
11.  Bij(\mBbbN{}a;A;f)
12.  \mforall{}i:\mBbbN{}a.  ((x  (f  i))  =  (y  (f  i)))
13.  aa  :  A
\mvdash{}  (x  aa)  =  (y  aa)


By

---

Latex:
xxxD  -3xxx

---

Home Index