Step
*
2
1
2
1
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|)))
2. a : ℚ
3. b : ℚ
4. c : ℚ
5. d : ℚ
6. qmax(c;d) ≤ b
7. a < b
⊢ |qmax(b;a) - qmax(d;c)| ≤ qmax(|b - d|;|a - c|)
BY
{ xxx((RWO "qmax_lb" (-2)) 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. (c ≤ b) ∧ (d ≤ b)
7. a < b
⊢ |qmax(b;a) - qmax(d;c)| ≤ qmax(|b - d|;|a - c|)
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.  qmax(c;d)  \mleq{}  b
7.  a  <  b
\mvdash{}  |qmax(b;a)  -  qmax(d;c)|  \mleq{}  qmax(|b  -  d|;|a  -  c|)
By
Latex:
xxx((RWO  "qmax\_lb"  (-2))  THENA  Auto)xxx
Home
Index