---

Step * 1 of Lemma uniform-continuity-from-fan3


1. [T] : Type
2. P : ℕ ⟶ ℙ@i'
3. a : ℕ@i'
4. P[a]
5. ∀n:ℕ. Dec(P[n])
6. h : T ⟶ {n:ℕ| P[n]} @i'
7. Bij(T;{n:ℕ| P[n]} ;h)
8. F : (ℕ ⟶ 𝔹) ⟶ T@i
9. {n:ℕ| P[n]}  ⊆r ℕ
⊢ ∃r:ℕ ⟶ {n:ℕ| P[n]} . ∀x:{n:ℕ| P[n]} . ((r x) = x ∈ {n:ℕ| P[n]} )
BY
{ (RenameVar `d' 5 THEN RepUR ``all decidable or`` 5) }

1
1. [T] : Type
2. P : ℕ ⟶ ℙ@i'
3. a : ℕ@i'
4. P[a]
5. d : n:ℕ ⟶ (P[n] + (¬P[n]))@i'
6. h : T ⟶ {n:ℕ| P[n]} @i'
7. Bij(T;{n:ℕ| P[n]} ;h)
8. F : (ℕ ⟶ 𝔹) ⟶ T@i
9. {n:ℕ| P[n]}  ⊆r ℕ
⊢ ∃r:ℕ ⟶ {n:ℕ| P[n]} . ∀x:{n:ℕ| P[n]} . ((r x) = x ∈ {n:ℕ| P[n]} )

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
3.  a  :  \mBbbN{}@i'
4.  P[a]
5.  \mforall{}n:\mBbbN{}.  Dec(P[n])
6.  h  :  T  {}\mrightarrow{}  \{n:\mBbbN{}|  P[n]\}  @i'
7.  Bij(T;\{n:\mBbbN{}|  P[n]\}  ;h)
8.  F  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T@i
9.  \{n:\mBbbN{}|  P[n]\}    \msubseteq{}r  \mBbbN{}
\mvdash{}  \mexists{}r:\mBbbN{}  {}\mrightarrow{}  \{n:\mBbbN{}|  P[n]\}  .  \mforall{}x:\{n:\mBbbN{}|  P[n]\}  .  ((r  x)  =  x)


By

---

Latex:
(RenameVar  `d'  5  THEN  RepUR  ``all  decidable  or``  5)

---

Home Index