Nuprl Definition : translation-group-fun
translation-group-fun(rv;e;T) ==
(∀s,t:ℝ. ∀x,y:Point. (T s x # T t y ⇒ (x # y ∨ s ≠ t)))
∧ (∀t,s:ℝ. ∀x:Point. T (t + s) x ≡ T t (T s x))
∧ (∀x:Point. ∀r:ℝ. ∃t:ℝ. (T t x ≡ x + r*e ∧ (∀y:ℝ. (y ≠ t ⇒ T y x # x + r*e))))
∧ (∀x:Point. ∀t:{t:ℝ| r0 ≤ t} . ∃r:{t:ℝ| r0 ≤ t} . T t x ≡ x + r*e)
Definitions occuring in Statement :
rv-mul: a*x,
rv-add: x + y,
rneq: x ≠ y,
rleq: x ≤ y,
radd: a + b,
int-to-real: r(n),
real: ℝ,
ss-eq: x ≡ y,
ss-sep: x # y,
ss-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
natural_number: $n
Definitions occuring in definition :
or: P ∨ Q,
radd: a + b,
and: P ∧ Q,
implies: P ⇒ Q,
rneq: x ≠ y,
ss-sep: x # y,
ss-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
real: ℝ,
rleq: x ≤ y,
int-to-real: r(n),
natural_number: $n,
ss-eq: x ≡ y,
apply: f a,
rv-add: x + y,
rv-mul: a*x
FDL editor aliases :
translation-group-fun
Latex:
translation-group-fun(rv;e;T) ==
(\mforall{}s,t:\mBbbR{}. \mforall{}x,y:Point. (T s x \# T t y {}\mRightarrow{} (x \# y \mvee{} s \mneq{} t)))
\mwedge{} (\mforall{}t,s:\mBbbR{}. \mforall{}x:Point. T (t + s) x \mequiv{} T t (T s x))
\mwedge{} (\mforall{}x:Point. \mforall{}r:\mBbbR{}. \mexists{}t:\mBbbR{}. (T t x \mequiv{} x + r*e \mwedge{} (\mforall{}y:\mBbbR{}. (y \mneq{} t {}\mRightarrow{} T y x \# x + r*e))))
\mwedge{} (\mforall{}x:Point. \mforall{}t:\{t:\mBbbR{}| r0 \mleq{} t\} . \mexists{}r:\{t:\mBbbR{}| r0 \mleq{} t\} . T t x \mequiv{} x + r*e)
Date html generated:
2017_10_05-AM-00_21_03
Last ObjectModification:
2017_06_26-PM-01_17_43
Theory : inner!product!spaces
Home
Index