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