Nuprl Definition : mset_fmon
mset_fmon(s) == <mset_mon{s}, λx:|s|. mset_inj{s}(x), λm.(λf:|s| ⟶ |m|. λy:MSet{s}. msFor{m} z ∈ y. (f z))>
Definitions occuring in Statement :
mset_for: mset_for,
mset_mon: mset_mon{s},
mset_inj: mset_inj{s}(x),
mset: MSet{s},
tlambda: λx:T. b[x],
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
pair: <a, b>,
grp_car: |g|,
set_car: |p|
Definitions occuring in definition :
mset_mon: mset_mon{s},
pair: <a, b>,
mset_inj: mset_inj{s}(x),
lambda: λx.A[x],
function: x:A ⟶ B[x],
set_car: |p|,
grp_car: |g|,
tlambda: λx:T. b[x],
mset: MSet{s},
mset_for: mset_for,
apply: f a
Latex:
mset\_fmon(s) ==
<mset\_mon\{s\}, \mlambda{}x:|s|. mset\_inj\{s\}(x), \mlambda{}m.(\mlambda{}f:|s| {}\mrightarrow{} |m|. \mlambda{}y:MSet\{s\}. msFor\{m\} z \mmember{} y. (f z))>
Date html generated:
2016_05_16-AM-07_48_30
Last ObjectModification:
2015_09_23-AM-09_52_10
Theory : mset
Home
Index