Nuprl Definition : mset
MSet{s} == as,bs:|s| List//(as ≡(|s|) bs)
Definitions occuring in Statement :
permr: as ≡(T) bs,
list: T List,
quotient: x,y:A//B[x; y],
set_car: |p|
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
list: T List,
permr: as ≡(T) bs,
set_car: |p|
Latex:
MSet\{s\} == as,bs:|s| List//(as \mequiv{}(|s|) bs)
Date html generated:
2016_05_16-AM-07_46_12
Last ObjectModification:
2015_09_23-AM-09_52_00
Theory : mset
Home
Index