---

Step * of Lemma r-triangle-inequality-rsub

∀[x,y:ℝ].  (|x - y| ≤ (|x| + |y|))
BY
{ (Auto THEN (InstLemma `r-triangle-inequality2` [⌜x⌝;⌜r0⌝;⌜y⌝]⋅ THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. |x - y| ≤ (|x - r0| + |r0 - y|)
⊢ |x - y| ≤ (|x| + |y|)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `r-triangle-inequality2`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index