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