Nuprl Lemma : real-vec-dist_wf
∀[n:ℕ]. ∀[x,y:ℝ^n].  (d(x;y) ∈ {d:ℝ| r0 ≤ d} )
Proof
Definitions occuring in Statement : 
real-vec-dist: d(x;y)
, 
real-vec: ℝ^n
, 
rleq: x ≤ y
, 
int-to-real: r(n)
, 
real: ℝ
, 
nat: ℕ
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
set: {x:A| B[x]} 
, 
natural_number: $n
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
real-vec-dist: d(x;y)
, 
prop: ℙ
Lemmas referenced : 
real-vec-norm-nonneg, 
real-vec-sub_wf, 
real-vec-norm_wf, 
rleq_wf, 
int-to-real_wf, 
real-vec_wf, 
nat_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
dependent_set_memberEquality, 
natural_numberEquality, 
axiomEquality, 
equalityTransitivity, 
equalitySymmetry, 
isect_memberEquality, 
because_Cache
Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (d(x;y)  \mmember{}  \{d:\mBbbR{}|  r0  \mleq{}  d\}  )
Date html generated:
2016_10_26-AM-10_24_37
Last ObjectModification:
2016_09_14-PM-06_28_59
Theory : reals
Home
Index