`∀[T:Type]. ∀[x,y:T ⟶ ℝ]. ∀[a,b:ℝ]. ∀[L:T List].`
`  (radd-list(map(λk.((a * x[k]) + (b * y[k]));L)) = ((a * radd-list(map(λk.x[k];L))) + (b * radd-list(map(λk.y[k];L)))))`

Proof

Definitions occuring in Statement :  req: `x = y` rmul: `a * b` radd: `a + b` radd-list: `radd-list(L)` real: `ℝ` map: `map(f;as)` list: `T List` uall: `∀[x:A]. B[x]` so_apply: `x[s]` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` implies: `P `` Q` all: `∀x:A. B[x]` top: `Top` prop: `ℙ` and: `P ∧ Q` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis applyEquality functionExtensionality because_Cache independent_isectElimination independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation rename functionEquality universeEquality natural_numberEquality productElimination

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[L:T  List].
(radd-list(map(\mlambda{}k.((a  *  x[k])  +  (b  *  y[k]));L))

Date html generated: 2017_10_02-PM-07_15_48
Last ObjectModification: 2017_07_28-AM-07_20_41

Theory : reals

Home Index