Nuprl Definition : tuple-equiv
tuple-equiv(L) == λt,t'. let n = ||L|| in ∀i:ℕn. ((snd(L[i])) t.i t'.i)
Definitions occuring in Statement :
select-tuple: x.n,
select: L[n],
length: ||as||,
int_seg: {i..j-},
let: let,
pi2: snd(t),
all: ∀x:A. B[x],
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
let: let,
length: ||as||,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
apply: f a,
pi2: snd(t),
select: L[n],
select-tuple: x.n
FDL editor aliases :
tuple-equiv
Latex:
tuple-equiv(L) == \mlambda{}t,t'. let n = ||L|| in \mforall{}i:\mBbbN{}n. ((snd(L[i])) t.i t'.i)
Date html generated:
2019_06_20-PM-02_16_32
Last ObjectModification:
2019_03_18-PM-03_51_43
Theory : tuples
Home
Index