Nuprl Definition : no_repeats

no_repeats(T;l) ==  ∀[i,j:ℕ].  (l[i] l[j] ∈ T)) supposing ((¬(i j ∈ ℕ)) and j < ||l|| and i < ||l||)

Definitions occuring in Statement :  select: L[n] length: ||as|| nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] not: ¬A equal: t ∈ T
Definitions occuring in definition :  uall: [x:A]. B[x] less_than: a < b length: ||as|| uimplies: supposing a nat: not: ¬A equal: t ∈ T select: L[n]
FDL editor aliases :  no_repeats

no\_repeats(T;l)  ==    \mforall{}[i,j:\mBbbN{}].    (\mneg{}(l[i]  =  l[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||l||  and  i  <  ||l||)

Date html generated: 2016_05_14-AM-06_36_13
Last ObjectModification: 2015_12_03-PM-02_08_34

Theory : list_0

Home Index