Nuprl Definition : permr
as ≡(T) bs == (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T))
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
,
int: ℤ
,
exists: ∃x:A. B[x]
,
sym_grp: Sym(n)
,
all: ∀x:A. B[x]
,
int_seg: {i..j-}
,
natural_number: $n
,
length: ||as||
,
equal: s = t ∈ T
,
apply: f a
,
perm_f: p.f
,
select: L[n]
Latex:
as \mequiv{}(T) bs == (||as|| = ||bs||) c\mwedge{} (\mexists{}p:Sym(||as||). \mforall{}i:\mBbbN{}||as||. (as[p.f i] = bs[i]))
Date html generated:
2016_05_16-AM-07_32_20
Last ObjectModification:
2015_09_23-AM-09_51_26
Theory : perms_2
Home
Index