Nuprl Definition : dislist
DisList{s} == {as:|s| List| ∀x:|s|. ((x #∈ as) ≤ 1)}
Definitions occuring in Statement :
count: a #∈ as,
list: T List,
le: A ≤ B,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
natural_number: $n,
set_car: |p|
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
all: ∀x:A. B[x],
set_car: |p|,
le: A ≤ B,
count: a #∈ as,
natural_number: $n
Latex:
DisList\{s\} == \{as:|s| List| \mforall{}x:|s|. ((x \#\mmember{} as) \mleq{} 1)\}
Date html generated:
2016_05_16-AM-07_39_51
Last ObjectModification:
2015_09_23-AM-09_51_40
Theory : list_2
Home
Index