### Nuprl Lemma : real-vec-norm_functionality

`∀[n:ℕ]. ∀[x,y:ℝ^n].  ||x|| = ||y|| supposing req-vec(n;x;y)`

Proof

Definitions occuring in Statement :  real-vec-norm: `||x||` req-vec: `req-vec(n;x;y)` real-vec: `ℝ^n` req: `x = y` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` real-vec-norm: `||x||` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  req_witness real-vec-norm_wf req-vec_wf real-vec_wf nat_wf dot-product_functionality rsqrt_wf dot-product-nonneg dot-product_wf rleq_wf int-to-real_wf req_weakening req_functionality rsqrt_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry independent_isectElimination dependent_set_memberEquality natural_numberEquality applyEquality productElimination

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    ||x||  =  ||y||  supposing  req-vec(n;x;y)

Date html generated: 2016_05_18-AM-09_48_28
Last ObjectModification: 2015_12_27-PM-11_12_17

Theory : reals

Home Index