Nuprl Definition : inner-product-space
InnerProductSpace ==
RealVectorSpace
"ip":{ip:Point ⟶ Point ⟶ ℝ|
(∀x1,x2,y1,y2:Point. (x1 ≡ x2 ⇒ y1 ≡ y2 ⇒ ((ip x1 y1) = (ip x2 y2))))
∧ (∀x,y:Point. ((ip x y) = (ip y x)))
∧ (∀x,y,z:Point. ((ip x + y z) = ((ip x z) + (ip y z))))
∧ (∀a:ℝ. ∀x,y:Point. ((ip a*x y) = (a * (ip x y))))}
"positive":∀x:Point. (x # 0 ⇐⇒ r0 < (self."ip" x x))
"perp":∀x:Point. (x # 0 ⇒ (∃y:Point. (y # 0 ∧ ((self."ip" x y) = r0))))
Definitions occuring in Statement :
rv-mul: a*x,
rv-add: x + y,
rv-0: 0,
real-vector-space: RealVectorSpace,
ss-eq: x ≡ y,
ss-sep: x # y,
ss-point: Point,
rless: x < y,
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
token: "$token",
record-select: r.x,
record+: record+
Definitions occuring in definition :
natural_number: $n,
int-to-real: r(n),
token: "$token",
record-select: r.x,
apply: f a,
req: x = y,
rv-0: 0,
ss-sep: x # y,
and: P ∧ Q,
ss-point: Point,
exists: ∃x:A. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
rless: x < y,
iff: P ⇐⇒ Q,
rmul: a * b,
rv-mul: a*x,
real: ℝ,
radd: a + b,
rv-add: x + y,
ss-eq: x ≡ y,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
real-vector-space: RealVectorSpace,
record+: record+
FDL editor aliases :
ip-sp
Latex:
InnerProductSpace ==
RealVectorSpace
"ip":\{ip:Point {}\mrightarrow{} Point {}\mrightarrow{} \mBbbR{}|
(\mforall{}x1,x2,y1,y2:Point. (x1 \mequiv{} x2 {}\mRightarrow{} y1 \mequiv{} y2 {}\mRightarrow{} ((ip x1 y1) = (ip x2 y2))))
\mwedge{} (\mforall{}x,y:Point. ((ip x y) = (ip y x)))
\mwedge{} (\mforall{}x,y,z:Point. ((ip x + y z) = ((ip x z) + (ip y z))))
\mwedge{} (\mforall{}a:\mBbbR{}. \mforall{}x,y:Point. ((ip a*x y) = (a * (ip x y))))\}
"positive":\mforall{}x:Point. (x \# 0 \mLeftarrow{}{}\mRightarrow{} r0 < (self."ip" x x))
"perp":\mforall{}x:Point. (x \# 0 {}\mRightarrow{} (\mexists{}y:Point. (y \# 0 \mwedge{} ((self."ip" x y) = r0))))
Date html generated:
2016_11_08-AM-09_14_31
Last ObjectModification:
2016_11_02-PM-02_46_15
Theory : inner!product!spaces
Home
Index