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: T 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: n - m,
add: n + m,
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_apply: x[s],
subtype_rel: A ⊆r 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