---

Step * of Lemma absval_sum

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (|Σ(f[x] | x < n)| ≤ Σ(|f[x]| | x < n))
BY
{ (SumInd THEN Try ((RWO "int-triangle-inequality" 0 THEN Auto THEN RWO "3" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    (|\mSigma{}(f[x]  |  x  <  n)|  \mleq{}  \mSigma{}(|f[x]|  |  x  <  n))


By

---

Latex:
(SumInd  THEN  Try  ((RWO  "int-triangle-inequality"  0  THEN  Auto  THEN  RWO  "3"  0  THEN  Auto)))

---

Home Index