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