### Nuprl Lemma : abmonoid_ac_1_fps

`∀[X:Type]. ∀[r:CRng]. ∀[a,b,c:PowerSeries(X;r)].  ((a+(b+c)) = (b+(a+c)) ∈ PowerSeries(X;r))`

Proof

Definitions occuring in Statement :  fps-add: `(f+g)` power-series: `PowerSeries(X;r)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache cumulativity natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination isect_memberEquality axiomEquality

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[a,b,c:PowerSeries(X;r)].    ((a+(b+c))  =  (b+(a+c)))

Date html generated: 2018_05_21-PM-09_56_48
Last ObjectModification: 2017_07_26-PM-06_33_06

Theory : power!series

Home Index