---

Step * 1 of Lemma qabs-difference-qmax

.....assertion..... 
∀a,b,c,d:ℚ.  ((b ≤ a) ⇒ (c ≤ a) ⇒ (d ≤ a) ⇒ (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|)))
BY
{ xxx(Auto
      THEN Unfold `qmax` 0
      THEN RepeatFor 3 (((SplitOnConclITE THENA Auto) THEN Try (((RWO "qle_complement_qorder" (-1)) THENA Auto))))
      THEN Auto)xxx }

1
.....truecase..... 
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. d : ℚ
5. b ≤ a
6. c ≤ a
7. d ≤ a
8. a ≤ b
9. d < c
10. |a - c| ≤ |b - d|
⊢ |b - c| ≤ |b - d|

2
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. d : ℚ
5. b ≤ a
6. c ≤ a
7. d ≤ a
8. a ≤ b
9. d < c
10. |b - d| < |a - c|
⊢ |b - c| ≤ |a - c|

3
.....truecase..... 
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. d : ℚ
5. b ≤ a
6. c ≤ a
7. d ≤ a
8. b < a
9. c ≤ d
10. |a - c| ≤ |b - d|
⊢ |a - d| ≤ |b - d|

4
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. d : ℚ
5. b ≤ a
6. c ≤ a
7. d ≤ a
8. b < a
9. c ≤ d
10. |b - d| < |a - c|
⊢ |a - d| ≤ |a - c|

---

Latex:

---

Latex:
.....assertion..... 
\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|)))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `qmax`  0
        THEN  RepeatFor  3  (((SplitOnConclITE  THENA  Auto)
                                              THEN  Try  (((RWO  "qle\_complement\_qorder"  (-1))  THENA  Auto))
                                              ))
        THEN  Auto)xxx

---

Home Index