---

Step * of Lemma weak-continuity-implies-strong1

(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ))))
⇒ (∀F:(ℕ ⟶ ℕ) ⟶ ℕ
      ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
         ∀f:ℕ ⟶ ℕ
           ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f)))))
BY
{ ((UnivCD THENA Auto) THEN RenameVar `W' 1 THEN (InstHyp [⌜F⌝] (-2)⋅ THENA Auto)) }

1
1. W : ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
⊢ ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
     ∀f:ℕ ⟶ ℕ. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f))))

---

Latex:

---

Latex:
(\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))))
{}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
            \00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}?)
                  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                      ((\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)))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RenameVar  `W'  1  THEN  (InstHyp  [\mkleeneopen{}F\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))

---

Home Index