---

Step * of Lemma strong-continuity-implies1-sp

∀[F:(ℕ ⟶ ℕ) ⟶ ℕ]. (↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?). ∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))))
BY
{ (UnivCD THENA Auto) }

1
1. F : (ℕ ⟶ ℕ) ⟶ ℕ
⊢ ↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?). ∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?)))

---

Latex:

---

Latex:
\mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}].  (\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:
(UnivCD  THENA  Auto)

---

Home Index