---

Step * 2 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|)))
⊢ ∀[a,b,c,d:ℚ].  (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|))
BY
{ xxx(Auto THEN (Decide qmax(c;d) ≤ qmax(a;b) THENA Auto))xxx }

1
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. qmax(c;d) ≤ qmax(a;b)
⊢ |qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|)

2
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. ¬(qmax(c;d) ≤ qmax(a;b))
⊢ |qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|)

---

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|)))
\mvdash{}  \mforall{}[a,b,c,d:\mBbbQ{}].    (|qmax(a;b)  -  qmax(c;d)|  \mleq{}  qmax(|a  -  c|;|b  -  d|))


By

---

Latex:
xxx(Auto  THEN  (Decide  qmax(c;d)  \mleq{}  qmax(a;b)  THENA  Auto))xxx

---

Home Index