Nuprl Definition : permr_upto
as ≡ bs upto x,y.R[x; y] == (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i]; bs[i]])
Definitions occuring in Statement :
sym_grp: Sym(n),
perm_f: p.f,
select: L[n],
length: ||as||,
int_seg: {i..j-},
cand: A c∧ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
cand: A c∧ B,
equal: s = t ∈ T,
int: ℤ,
exists: ∃x:A. B[x],
sym_grp: Sym(n),
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
apply: f a,
perm_f: p.f,
select: L[n]
Latex:
as \mequiv{} bs upto x,y.R[x; y] == (||as|| = ||bs||) c\mwedge{} (\mexists{}p:Sym(||as||). \mforall{}i:\mBbbN{}||as||. R[as[p.f i]; bs[i]])
Date html generated:
2016_05_16-AM-07_34_07
Last ObjectModification:
2015_09_23-AM-09_51_27
Theory : perms_2
Home
Index