Step
*
of Lemma
l_sum-triangle-inequality
∀[T:Type]. ∀[L:T List]. ∀[f,g:T ⟶ ℤ].
(|l_sum(map(λa.f[a];L)) - l_sum(map(λa.g[a];L))| ≤ l_sum(map(λa.|f[a] - g[a]|;L)))
BY
{ ((InstLemma `l_sum-triangle-inequality-general` [] THEN RepeatFor 2 (ParallelLast'))
THEN (InstHyp [⌜0⌝;⌜0⌝] (-1)⋅ THENA Auto)
THEN RepeatFor 2 (ParallelLast')
THEN NthHypEq (-1)
THEN EqCD
THEN Auto
THEN Subst' |0 - 0| ~ 0 0
THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[L:T List]. \mforall{}[f,g:T {}\mrightarrow{} \mBbbZ{}].
(|l\_sum(map(\mlambda{}a.f[a];L)) - l\_sum(map(\mlambda{}a.g[a];L))| \mleq{} l\_sum(map(\mlambda{}a.|f[a] - g[a]|;L)))
By
Latex:
((InstLemma `l\_sum-triangle-inequality-general` [] THEN RepeatFor 2 (ParallelLast'))
THEN (InstHyp [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN RepeatFor 2 (ParallelLast')
THEN NthHypEq (-1)
THEN EqCD
THEN Auto
THEN Subst' |0 - 0| \msim{} 0 0
THEN Auto)
Home
Index