---

Step * of Lemma Minkowski-inequality1

∀[n:ℕ]. ∀[x,y:ℝ^n].  (||x + y|| ≤ (||x|| + ||y||))
BY
{ (Auto
   THEN ((InstLemma `rnexp-rleq-iff` [⌜||x + y||⌝;⌜||x|| + ||y||⌝;⌜2⌝]⋅ THENM (BHyp -1  THEN Thin (-1)))
         THENA (Auto THEN (Assert (r0 ≤ ||x||) ∧ (r0 ≤ ||y||) BY Auto) THEN D -1 THEN nRAdd ⌜||x||⌝ (-1)⋅ THEN Auto)
         )
   ) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
⊢ ||x + y||^2 ≤ ||x|| + ||y||^2

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rnexp-rleq-iff`  [\mkleeneopen{}||x  +  y||\mkleeneclose{};\mkleeneopen{}||x||  +  ||y||\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
              THENM  (BHyp  -1    THEN  Thin  (-1))
              )
              THENA  (Auto
                            THEN  (Assert  (r0  \mleq{}  ||x||)  \mwedge{}  (r0  \mleq{}  ||y||)  BY
                                                    Auto)
                            THEN  D  -1
                            THEN  nRAdd  \mkleeneopen{}||x||\mkleeneclose{}  (-1)\mcdot{}
                            THEN  Auto)
              )
  )

---

Home Index