Nuprl Definition : finite_set
FiniteSet{s} == {a:MSet{s}| ∀x:|s|. ((x #∈ a) ≤ 1)}
Definitions occuring in Statement :
mset_count: x #∈ a,
mset: MSet{s},
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]} ,
mset: MSet{s},
all: ∀x:A. B[x],
set_car: |p|,
le: A ≤ B,
mset_count: x #∈ a,
natural_number: $n
FDL editor aliases :
finite_set
Latex:
FiniteSet\{s\} == \{a:MSet\{s\}| \mforall{}x:|s|. ((x \#\mmember{} a) \mleq{} 1)\}
Date html generated:
2016_05_16-AM-07_46_28
Last ObjectModification:
2015_09_23-AM-09_52_01
Theory : mset
Home
Index