---

Step * of Lemma rv-norm-triangle-inequality

No Annotations
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (||x + y|| ≤ (||x|| + ||y||))
BY
{ (Auto THEN (InstLemma `rnexp-rleq-iff` [⌜||x + y||⌝;⌜||x|| + ||y||⌝;⌜2⌝]⋅ THENA Auto) THEN BHyp -1 THEN Thin (-1)) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
⊢ ||x + y||^2 ≤ ||x|| + ||y||^2

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[x,y:Point(rv)].    (||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{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  Thin  (-1))

---

Home Index