Nuprl Lemma : polynom_alg_wf
∀S:DSet. ∀A:CRng.  (polynom_alg{i:l}(S;A) ∈ 𝕌')
Proof
Definitions occuring in Statement : 
polynom_alg: polynom_alg{i:l}(S;A)
, 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
universe: Type
, 
crng: CRng
, 
dset: DSet
Definitions unfolded in proof : 
polynom_alg: polynom_alg{i:l}(S;A)
, 
all: ∀x:A. B[x]
, 
member: t ∈ T
Lemmas referenced : 
free_abmonoid_wf, 
fmonalg_wf, 
free_abmon_mon_wf, 
crng_wf, 
dset_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
sqequalReflexivity, 
sqequalTransitivity, 
computationStep, 
lambdaFormation, 
cut, 
productEquality, 
lemma_by_obid, 
sqequalHypSubstitution, 
dependent_functionElimination, 
thin, 
hypothesisEquality, 
hypothesis
Latex:
\mforall{}S:DSet.  \mforall{}A:CRng.    (polynom\_alg\{i:l\}(S;A)  \mmember{}  \mBbbU{}')
Date html generated:
2016_05_16-AM-08_14_30
Last ObjectModification:
2015_12_28-PM-06_09_14
Theory : polynom_1
Home
Index