Nuprl Definition : is-isometry
is-isometry(rv;f) == ∃g:Point ⟶ Point. ∃t:Point. (Orthogonal(g) ∧ (∀x:Point. f x ≡ g x + t))
Definitions occuring in Statement :
rv-orthogonal: Orthogonal(f),
rv-add: x + y,
ss-eq: x ≡ y,
ss-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
rv-orthogonal: Orthogonal(f),
all: ∀x:A. B[x],
ss-point: Point,
ss-eq: x ≡ y,
rv-add: x + y,
apply: f a
FDL editor aliases :
is-isometry
Latex:
is-isometry(rv;f) == \mexists{}g:Point {}\mrightarrow{} Point. \mexists{}t:Point. (Orthogonal(g) \mwedge{} (\mforall{}x:Point. f x \mequiv{} g x + t))
Date html generated:
2017_10_04-PM-11_53_54
Last ObjectModification:
2017_03_23-PM-03_52_47
Theory : inner!product!spaces
Home
Index