---

Step * 2 2 1 2 1 of Lemma qabs-difference-qmax


1. ∀a,b,c,d:ℚ.  ((b ≤ a) ⇒ (c ≤ a) ⇒ (d ≤ a) ⇒ (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|)))
2. a : ℚ
3. b : ℚ
4. c : ℚ
5. d : ℚ
6. a < d ∧ b < d
7. c ≤ d
8. |qmax(d;c) - qmax(b;a)| ≤ qmax(|d - b|;|c - a|)
⊢ |qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|)
BY
{ xxx((RWO "qmax-symmetry" 0 THENA Auto)
      THEN (NthHypEq (-1))
      THEN RepeatFor 2 ((EqCD THEN Auto THEN Try ((BLemma `qabs-difference-symmetry` THEN Auto)))))xxx }

---

Latex:

---

Latex:

1.  \mforall{}a,b,c,d:\mBbbQ{}.    ((b  \mleq{}  a)  {}\mRightarrow{}  (c  \mleq{}  a)  {}\mRightarrow{}  (d  \mleq{}  a)  {}\mRightarrow{}  (|qmax(a;b)  -  qmax(c;d)|  \mleq{}  qmax(|a  -  c|;|b  -  d|)))
2.  a  :  \mBbbQ{}
3.  b  :  \mBbbQ{}
4.  c  :  \mBbbQ{}
5.  d  :  \mBbbQ{}
6.  a  <  d  \mwedge{}  b  <  d
7.  c  \mleq{}  d
8.  |qmax(d;c)  -  qmax(b;a)|  \mleq{}  qmax(|d  -  b|;|c  -  a|)
\mvdash{}  |qmax(a;b)  -  qmax(c;d)|  \mleq{}  qmax(|a  -  c|;|b  -  d|)


By

---

Latex:
xxx((RWO  "qmax-symmetry"  0  THENA  Auto)
        THEN  (NthHypEq  (-1))
        THEN  RepeatFor  2  ((EqCD  THEN  Auto  THEN  Try  ((BLemma  `qabs-difference-symmetry`  THEN  Auto)))))xxx

---

Home Index