Nuprl Definition : mset_union_mon
<MSet{s},⋃,0> == <MSet{s}, λx,y. eq_mset{s}(x,y), λx,y. tt, λx,y. (x ⋃ y), 0{s}, λx.x>
Definitions occuring in Statement :
mset_union: a ⋃ b,
eq_mset: eq_mset{s}(a,b),
null_mset: 0{s},
mset: MSet{s},
btrue: tt,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
mset: MSet{s},
eq_mset: eq_mset{s}(a,b),
btrue: tt,
mset_union: a ⋃ b,
pair: <a, b>,
null_mset: 0{s},
lambda: λx.A[x]
Latex:
<MSet\{s\},\mcup{},0> == <MSet\{s\}, \mlambda{}x,y. eq\_mset\{s\}(x,y), \mlambda{}x,y. tt, \mlambda{}x,y. (x \mcup{} y), 0\{s\}, \mlambda{}x.x>
Date html generated:
2016_05_16-AM-07_49_27
Last ObjectModification:
2015_09_23-AM-09_52_15
Theory : mset
Home
Index