Nuprl Lemma : real-vec-dist-dim0
∀[x,y:Top]. (d(x;y) = r0)
Proof
Definitions occuring in Statement :
real-vec-dist: d(x;y),
req: x = y,
int-to-real: r(n),
uall: ∀[x:A]. B[x],
top: Top,
natural_number: $n
Definitions unfolded in proof :
real-vec-dist: d(x;y),
real-vec-norm: ||x||,
dot-product: x⋅y,
subtract: n - m,
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
top: Top,
so_apply: x[s],
uimplies: b supposing a,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
and: P ∧ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
implies: P ⇒ Q
Lemmas referenced :
rsum-empty,
istype-void,
rsqrt0,
req_witness,
rsqrt_wf,
rleq_weakening_equal,
int-to-real_wf,
rleq_wf,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
minusEquality,
isect_memberEquality_alt,
voidElimination,
hypothesis,
independent_isectElimination,
independent_pairFormation,
imageMemberEquality,
hypothesisEquality,
baseClosed,
isect_memberFormation_alt,
because_Cache,
dependent_set_memberEquality_alt,
universeIsType,
applyEquality,
independent_functionElimination,
inhabitedIsType,
isectIsTypeImplies
Latex:
\mforall{}[x,y:Top]. (d(x;y) = r0)
Date html generated:
2019_10_30-AM-08_28_11
Last ObjectModification:
2019_06_21-PM-04_59_44
Theory : reals
Home
Index