Nuprl Lemma : Cauchy-Schwarz
∀[n:ℕ]. ∀[x,y:ℝ^n]. (|x ⋅ y| ≤ (||x|| * ||y||))
Proof
Definitions occuring in Statement :
real-vec-norm: ||x||,
dot-product: x ⋅ y,
real-vec: ℝ^n,
rleq: x ≤ y,
rabs: |x|,
rmul: a * b,
nat: ℕ,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
real-vec: ℝ^n,
so_apply: x[s],
dot-product: x ⋅ y,
real-vec-norm: ||x||
Lemmas referenced :
Cauchy-Schwarz3,
real-vec_wf,
nat_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[x,y:\mBbbR{}\^{}n]. (|x \mcdot{} y| \mleq{} (||x|| * ||y||))
Date html generated:
2016_05_18-AM-09_49_09
Last ObjectModification:
2015_12_27-PM-11_10_47
Theory : reals
Home
Index