---

Step * of Lemma q-triangle-inequality3

∀[x,y,a,b:ℚ].  (|x + y| ≤ (a + b)) supposing ((|y| ≤ b) and (|x| ≤ a))
BY
{ (Auto
   THEN (InstLemma `q-triangle-inequality` [⌜x⌝;⌜y⌝]⋅ THENA Auto)
   THEN ((RWO "-3" (-1)) THENA Auto)
   THEN (RWO "-2" (-1))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y,a,b:\mBbbQ{}].    (|x  +  y|  \mleq{}  (a  +  b))  supposing  ((|y|  \mleq{}  b)  and  (|x|  \mleq{}  a))


By

---

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

---

Home Index