Nuprl Lemma : real-vec-dist-dilation

[n:ℕ]. ∀[x,y:ℝ^n]. ∀[a:ℝ].  (d(a*x;a*y) (|a| d(x;y)))


Proof




Definitions occuring in Statement :  real-vec-dist: d(x;y) real-vec-mul: a*X real-vec: ^n rabs: |x| req: y rmul: b real: nat: uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T real-vec-dist: d(x;y) subtype_rel: A ⊆B prop: implies:  Q real-vec-sub: Y real-vec-mul: a*X req-vec: req-vec(n;x;y) all: x:A. B[x] nat: real-vec: ^n uimplies: supposing a rsub: y and: P ∧ Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  req_witness real-vec-dist_wf real-vec-mul_wf real_wf rleq_wf int-to-real_wf rmul_wf rabs_wf real-vec_wf nat_wf int_seg_wf req_wf radd_wf rminus_wf req_weakening uiff_transitivity req_functionality req_transitivity rmul-distrib radd_functionality rmul_over_rminus rminus_functionality rmul_comm real-vec-norm_wf real-vec-sub_wf real-vec-norm-mul real-vec-norm_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality setElimination rename setEquality natural_numberEquality sqequalRule independent_functionElimination isect_memberEquality because_Cache lambdaFormation independent_isectElimination productElimination

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].  \mforall{}[a:\mBbbR{}].    (d(a*x;a*y)  =  (|a|  *  d(x;y)))



Date html generated: 2016_10_26-AM-10_26_55
Last ObjectModification: 2016_09_28-PM-00_36_44

Theory : reals


Home Index