Nuprl Lemma : l_sum-triangle-inequality-general

[T:Type]. ∀[L:T List]. ∀[x,y:ℤ]. ∀[f,g:T ⟶ ℤ].
  (|(l_sum(map(λa.f[a];L)) x) l_sum(map(λa.g[a];L)) y| ≤ (l_sum(map(λa.|f[a] g[a]|;L)) |x y|))


Proof




Definitions occuring in Statement :  l_sum: l_sum(L) map: map(f;as) list: List absval: |i| uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B lambda: λx.A[x] function: x:A ⟶ B[x] subtract: m add: m int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_apply: x[s] subtype_rel: A ⊆B nat: so_lambda: λ2x.t[x]
Lemmas referenced :  list_accum-triangle-inequality list_wf absval_wf subtract_wf nat_wf l_sum_as_accum
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality functionEquality intEquality universeEquality lambdaEquality applyEquality setElimination rename sqequalRule

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[x,y:\mBbbZ{}].  \mforall{}[f,g:T  {}\mrightarrow{}  \mBbbZ{}].
    (|(l\_sum(map(\mlambda{}a.f[a];L))  +  x)  -  l\_sum(map(\mlambda{}a.g[a];L))  +  y|  \mleq{}  (l\_sum(map(\mlambda{}a.|f[a]  -  g[a]|;L))
      +  |x  -  y|))



Date html generated: 2016_05_14-PM-02_53_51
Last ObjectModification: 2015_12_26-PM-02_33_48

Theory : list_1


Home Index