---

Step * of Lemma r-triangle-inequality2

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

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

---

Latex:

---

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


By

---

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

---

Home Index