### Nuprl Lemma : ni-iterated-min_wf

`∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ∞].  (ni-iterated-min(n;f) ∈ ℕ∞)`

Proof

Definitions occuring in Statement :  ni-iterated-min: `ni-iterated-min(n;f)` nat-inf: `ℕ∞` 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` ni-iterated-min: `ni-iterated-min(n;f)` nat: `ℕ`
Lemmas referenced :  primrec_wf nat-inf_wf nat-inf-infinity_wf ni-min_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality lambdaEquality applyEquality natural_numberEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality because_Cache

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}\minfty{}].    (ni-iterated-min(n;f)  \mmember{}  \mBbbN{}\minfty{})

Date html generated: 2016_05_15-PM-01_48_47
Last ObjectModification: 2015_12_27-AM-00_08_50

Theory : basic

Home Index