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: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
less_than: a < b,
length: ||as||,
uimplies: b supposing a,
nat: ℕ,
not: ¬A,
equal: s = t ∈ T,
select: L[n]
FDL editor aliases :
no_repeats
Latex:
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