Nuprl Definition : old_no_repeats
old_no_repeats(T; l) == ∀i,j:ℕ. (i < ||l||
⇒ j < ||l||
⇒ (¬(i = j ∈ ℕ))
⇒ (¬(l[i] = l[j] ∈ T)))
Definitions occuring in Statement :
select: L[n]
,
length: ||as||
,
nat: ℕ
,
less_than: a < b
,
all: ∀x:A. B[x]
,
not: ¬A
,
implies: P
⇒ Q
,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x]
,
less_than: a < b
,
length: ||as||
,
implies: P
⇒ Q
,
nat: ℕ
,
not: ¬A
,
equal: s = t ∈ T
,
select: L[n]
Latex:
old\_no\_repeats(T; l) == \mforall{}i,j:\mBbbN{}. (i < ||l|| {}\mRightarrow{} j < ||l|| {}\mRightarrow{} (\mneg{}(i = j)) {}\mRightarrow{} (\mneg{}(l[i] = l[j])))
Date html generated:
2016_05_15-PM-01_54_50
Last ObjectModification:
2015_09_23-AM-07_37_25
Theory : list!
Home
Index