---

Step * 2 of Lemma uniform-continuity-from-fan


1. [T] : Type
2. F : (ℕ ⟶ 𝔹) ⟶ T
3. M : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?)
4. [%2] : ∀f:ℕ ⟶ 𝔹
            ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f)))
5. n : ℕ
6. s : ℕn ⟶ 𝔹
⊢ Dec(↑isl(M n s))
BY
{ Auto }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  F  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T
3.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  (T?)
4.  [\%2]  :  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}
                        ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))  \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f)))
5.  n  :  \mBbbN{}
6.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  Dec(\muparrow{}isl(M  n  s))


By

---

Latex:
Auto

---

Home Index