Nuprl Definition : rv-orthogonal
Orthogonal(f) == (∀x,y:Point. (f x + y ≡ f x + f y ∧ (x ⋅ y = f x ⋅ f y))) ∧ (∀x:Point. ∀a:ℝ. f a*x ≡ a*f x)
Definitions occuring in Statement :
rv-ip: x ⋅ y,
rv-mul: a*x,
rv-add: x + y,
ss-eq: x ≡ y,
ss-point: Point,
req: x = y,
real: ℝ,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
apply: f a,
rv-mul: a*x,
ss-eq: x ≡ y,
real: ℝ,
all: ∀x:A. B[x],
ss-point: Point,
rv-ip: x ⋅ y,
req: x = y,
rv-add: x + y,
and: P ∧ Q
FDL editor aliases :
rv-orthogonal
Latex:
Orthogonal(f) ==
(\mforall{}x,y:Point. (f x + y \mequiv{} f x + f y \mwedge{} (x \mcdot{} y = f x \mcdot{} f y))) \mwedge{} (\mforall{}x:Point. \mforall{}a:\mBbbR{}. f a*x \mequiv{} a*f x)
Date html generated:
2016_11_08-AM-09_17_39
Last ObjectModification:
2016_10_31-PM-11_40_09
Theory : inner!product!spaces
Home
Index