Nuprl Lemma : mdist-rn-prod-metric
∀[k,x,y:Top]. (mdist(rn-prod-metric(k);x;y) ~ Σ{|(x i) - y i| | 0≤i≤k - 1})
Proof
Definitions occuring in Statement :
rn-prod-metric: rn-prod-metric(n),
mdist: mdist(d;x;y),
rsum: Σ{x[k] | n≤k≤m},
rabs: |x|,
rsub: x - y,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
subtract: n - m,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
prod-metric: prod-metric(k;d),
rmetric: rmetric(),
mdist: mdist(d;x;y),
rn-prod-metric: rn-prod-metric(n)
Lemmas referenced :
istype-top
Rules used in proof :
hypothesis,
extract_by_obid,
isectIsTypeImplies,
thin,
isectElimination,
isect_memberEquality_alt,
sqequalHypSubstitution,
hypothesisEquality,
inhabitedIsType,
axiomSqEquality,
cut,
introduction,
isect_memberFormation_alt,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}[k,x,y:Top]. (mdist(rn-prod-metric(k);x;y) \msim{} \mSigma{}\{|(x i) - y i| | 0\mleq{}i\mleq{}k - 1\})
Date html generated:
2019_10_30-AM-08_34_04
Last ObjectModification:
2019_10_27-PM-04_54_30
Theory : reals
Home
Index