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