---

Step * 1 of Lemma strong-continuity-implies1-sp


1. F : (ℕ ⟶ ℕ) ⟶ ℕ
⊢ ↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?). ∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?)))
BY
{ (InstLemma `strong-continuity-implies1` [⌜F⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mdownarrow{}\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}?).  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))


By

---

Latex:
(InstLemma  `strong-continuity-implies1`  [\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index