Nuprl Lemma : linearization_wf

`∀[p:iPolynomial()]. ∀[L:ℤ List List].  (linearization(p;L) ∈ {cs:ℤ List| ||cs|| = ||L|| ∈ ℤ} )`

Proof

Definitions occuring in Statement :  linearization: `linearization(p;L)` iPolynomial: `iPolynomial()` length: `||as||` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` linearization: `linearization(p;L)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` prop: `ℙ`
Lemmas referenced :  map_length list_wf poly-coeff-of_wf map_wf equal-wf-base list_subtype_base int_subtype_base iPolynomial_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis because_Cache lambdaEquality hypothesisEquality dependent_set_memberEquality baseApply closedConclusion baseClosed applyEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[p:iPolynomial()].  \mforall{}[L:\mBbbZ{}  List  List].    (linearization(p;L)  \mmember{}  \{cs:\mBbbZ{}  List|  ||cs||  =  ||L||\}  )

Date html generated: 2017_04_14-AM-09_03_49
Last ObjectModification: 2017_02_27-PM-03_44_01

Theory : omega

Home Index