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