Step
*
of Lemma
qabs-difference-qmax
∀[a,b,c,d:ℚ].  (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|))
BY
{ xxxAssert ⌜∀a,b,c,d:ℚ.  ((b ≤ a) 
⇒ (c ≤ a) 
⇒ (d ≤ a) 
⇒ (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|)))⌝⋅xxx }
1
.....assertion..... 
∀a,b,c,d:ℚ.  ((b ≤ a) 
⇒ (c ≤ a) 
⇒ (d ≤ a) 
⇒ (|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|)))
⊢ ∀[a,b,c,d:ℚ].  (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|))
Latex:
Latex:
\mforall{}[a,b,c,d:\mBbbQ{}].    (|qmax(a;b)  -  qmax(c;d)|  \mleq{}  qmax(|a  -  c|;|b  -  d|))
By
Latex:
xxxAssert  \mkleeneopen{}\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|)))\mkleeneclose{}
\mcdot{}xxx
Home
Index