Step
*
1
of Lemma
markov-streamless-function
.....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))
BY
{ xxx(ExRepD THEN (Assert ℕa ~ A BY (RelRST THEN Auto)) THEN D -1)xxx }
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. Bij(ℕa;A;f)
⊢ Dec(x = y ∈ (A ⟶ B))
Latex:
Latex:
.....decidable?.....
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. \mexists{}a:\mBbbN{}. A \msim{} \mBbbN{}a
5. \mforall{}x,y:B. Dec(x = y)
6. \mneg{}\mneg{}(\mexists{}n:\mBbbN{}. B \msim{} \mBbbN{}n)
7. x : A {}\mrightarrow{} B
8. y : A {}\mrightarrow{} B
\mvdash{} Dec(x = y)
By
Latex:
xxx(ExRepD THEN (Assert \mBbbN{}a \msim{} A BY (RelRST THEN Auto)) THEN D -1)xxx
Home
Index