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