Nuprl Definition : translation-group
translation-group(rv;e;T) == mk-s-subgroup(Perm(rv);fg.∃t:ℝ. ∀x:Point. (fst(fg)) x ≡ T t x)
Definitions occuring in Statement :
rv-permutation-group: Perm(rv),
real: ℝ,
mk-s-subgroup: mk-s-subgroup(sg;x.P[x]),
ss-eq: x ≡ y,
ss-point: Point,
pi1: fst(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a
Definitions occuring in definition :
mk-s-subgroup: mk-s-subgroup(sg;x.P[x]),
rv-permutation-group: Perm(rv),
exists: ∃x:A. B[x],
real: ℝ,
all: ∀x:A. B[x],
ss-point: Point,
ss-eq: x ≡ y,
pi1: fst(t),
apply: f a
FDL editor aliases :
translation-group
Latex:
translation-group(rv;e;T) == mk-s-subgroup(Perm(rv);fg.\mexists{}t:\mBbbR{}. \mforall{}x:Point. (fst(fg)) x \mequiv{} T t x)
Date html generated:
2017_10_05-AM-00_21_55
Last ObjectModification:
2017_06_24-PM-03_37_30
Theory : inner!product!spaces
Home
Index