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