Nuprl Lemma : qabs-difference-qmax
∀[a,b,c,d:ℚ]. (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|))
Proof
Definitions occuring in Statement :
qabs: |r|,
qmax: qmax(x;y),
qle: r ≤ s,
qsub: r - s,
rationals: ℚ,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
qmax: qmax(x;y),
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
true: True,
uiff: uiff(P;Q),
and: P ∧ Q,
guard: {T},
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
squash: ↓T,
qabs: |r|,
callbyvalueall: callbyvalueall,
has-value: (a)↓,
has-valueall: has-valueall(a),
subtype_rel: A ⊆r B,
not: ¬A,
false: False,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
qsub: r - s,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
bnot: ¬bb,
assert: ↑b,
rev_uimplies: rev_uimplies(P;Q),
evalall: evalall(t),
qpositive: qpositive(r),
lt_int: i <z j,
qmul: r * s,
decidable: Dec(P)
Lemmas referenced :
qle_wf,
rationals_wf,
q_le_wf,
bool_wf,
equal-wf-T-base,
assert_wf,
qabs_wf,
qsub_wf,
qle_weakening_eq_qorder,
bnot_wf,
not_wf,
qle_complement_qorder,
qle_weakening_lt_qorder,
uiff_transitivity2,
eqtt_to_assert,
assert-q_le-eq,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot,
squash_wf,
true_wf,
equal_wf,
qle_antisymmetry,
valueall-type-has-valueall,
rationals-valueall-type,
evalall-reduce,
qpositive_wf,
qless_wf,
int-subtype-rationals,
qless_complement_qorder,
assert-qpositive,
iff_transitivity,
iff_weakening_uiff,
qadd_preserves_qless,
qmul_wf,
qadd_wf,
qadd_preserves_qle,
qadd_comm_q,
qadd_ac_1_q,
qinverse_q,
mon_ident_q,
iff_weakening_equal,
qless_transitivity_2_qorder,
qless_irreflexivity,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
qless_transitivity,
qless_transitivity_1_qorder,
qle_transitivity_qorder,
qmul_over_plus_qrng,
qinv_inv_q,
mon_assoc_q,
qadd_inv_assoc_q,
zero-qle-qabs,
decidable__qle,
qmax_wf,
qle_witness,
qmax_lb,
qmax-symmetry,
qmax_strict_lb,
qabs-qminus,
qminus-qsub
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
equalityTransitivity,
equalitySymmetry,
baseClosed,
because_Cache,
independent_isectElimination,
natural_numberEquality,
productElimination,
unionElimination,
equalityElimination,
independent_functionElimination,
sqequalRule,
applyEquality,
lambdaEquality,
imageElimination,
universeEquality,
imageMemberEquality,
dependent_functionElimination,
hyp_replacement,
applyLambdaEquality,
callbyvalueReduce,
voidElimination,
independent_pairFormation,
impliesFunctionality,
minusEquality,
dependent_pairFormation,
promote_hyp,
instantiate,
cumulativity,
isect_memberFormation,
isect_memberEquality,
productEquality
Latex:
\mforall{}[a,b,c,d:\mBbbQ{}]. (|qmax(a;b) - qmax(c;d)| \mleq{} qmax(|a - c|;|b - d|))
Date html generated:
2018_05_21-PM-11_57_52
Last ObjectModification:
2017_07_26-PM-06_47_44
Theory : rationals
Home
Index