### Nuprl Lemma : mk-finite-nat-seq_wf

`∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ].  (f^(n) ∈ finite-nat-seq())`

Proof

Definitions occuring in Statement :  mk-finite-nat-seq: `f^(n)` finite-nat-seq: `finite-nat-seq()` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` mk-finite-nat-seq: `f^(n)` finite-nat-seq: `finite-nat-seq()` nat: `ℕ`
Lemmas referenced :  nat_wf int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule dependent_pairEquality hypothesisEquality functionEquality lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].    (f\^{}(n)  \mmember{}  finite-nat-seq())

Date html generated: 2016_05_14-PM-09_54_32
Last ObjectModification: 2016_01_15-AM-07_44_28

Theory : continuity

Home Index