### Nuprl Lemma : int-prod_wf_nat

`∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ].  (Π(f[x] | x < n) ∈ ℕ)`

Proof

Definitions occuring in Statement :  int-prod: `Π(f[x] | x < k)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int-prod: `Π(f[x] | x < k)` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B`
Lemmas referenced :  primrec_wf nat_wf false_wf le_wf mul_bounds_1a int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation lambdaEquality multiplyEquality setElimination rename applyEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].    (\mPi{}(f[x]  |  x  <  n)  \mmember{}  \mBbbN{})

Date html generated: 2016_05_14-AM-07_33_49
Last ObjectModification: 2015_12_26-PM-01_23_43

Theory : int_2

Home Index