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