Nuprl Lemma : radd-list-linearity1

[T:Type]. ∀[x,y:T ⟶ ℝ]. ∀[L:T List].
  (radd-list(map(λk.(x[k] y[k]);L)) (radd-list(map(λk.x[k];L)) radd-list(map(λk.y[k];L))))


Proof




Definitions occuring in Statement :  req: y radd: b radd-list: radd-list(L) real: map: map(f;as) list: 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 ⊆B uimplies: supposing a implies:  Q all: x:A. B[x] top: Top prop: uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  list_induction req_wf radd-list_wf-bag map_wf real_wf radd_wf list-subtype-bag list_wf map_nil_lemma radd_list_nil_lemma map_cons_lemma req_witness subtype_rel_self int-to-real_wf req_weakening cons_wf req_functionality radd-int req_transitivity radd-list-cons radd_functionality uiff_transitivity req_inversion radd-assoc radd-ac radd_comm
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 addEquality productElimination

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



Date html generated: 2017_10_02-PM-07_15_52
Last ObjectModification: 2017_07_28-AM-07_20_44

Theory : reals


Home Index