---

Step * of Lemma Minkowski-inequality2

∀[n:ℕ]. ∀[x,y:ℝ^n].  (||x - y|| ≤ (||x|| + ||y||))
BY
{ (Auto
   THEN (InstLemma `Minkowski-inequality1` [⌜n⌝;⌜x⌝;⌜r(-1)*y⌝]⋅ THENA Auto)
   THEN (RWO "real-vec-norm-mul" (-1)⋅ THENA Auto)
   THEN (RWO  "rabs-int" (-1) THENA Auto)
   THEN RepUR ``absval`` -1
   THEN nRNorm (-1)
   THEN (RWO "-1<" 0 THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. ||x + r(-1)*y|| ≤ (||x|| + ||y||)
⊢ ||x - y|| ≤ ||x + r(-1)*y||

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (||x  -  y||  \mleq{}  (||x||  +  ||y||))


By

---

Latex:
(Auto
  THEN  (InstLemma  `Minkowski-inequality1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}r(-1)*y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "real-vec-norm-mul"  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO    "rabs-int"  (-1)  THENA  Auto)
  THEN  RepUR  ``absval``  -1
  THEN  nRNorm  (-1)
  THEN  (RWO  "-1<"  0  THENA  Auto))

---

Home Index