---

Step * of Lemma q-triangle-inequality2

∀[x,y,z:ℚ].  (|x - z| ≤ (|x - y| + |y - z|))
BY
{ (Auto THEN (InstLemma `q-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:\mBbbQ{}].    (|x  -  z|  \mleq{}  (|x  -  y|  +  |y  -  z|))


By

---

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

---

Home Index