Nuprl Definition : maximal-sub-bag
maximal-sub-bag(T;m;b;s.P[s]) == (∀s:bag(T). (sub-bag(T;s;b) ⇒ P[s] ⇒ sub-bag(T;s;m))) ∧ P[m]
Definitions occuring in Statement :
sub-bag: sub-bag(T;as;bs),
bag: bag(T),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
bag: bag(T),
implies: P ⇒ Q,
sub-bag: sub-bag(T;as;bs)
FDL editor aliases :
maximal-sub-bag
Latex:
maximal-sub-bag(T;m;b;s.P[s]) == (\mforall{}s:bag(T). (sub-bag(T;s;b) {}\mRightarrow{} P[s] {}\mRightarrow{} sub-bag(T;s;m))) \mwedge{} P[m]
Date html generated:
2018_05_21-PM-06_24_32
Last ObjectModification:
2018_01_08-AM-00_32_08
Theory : bags
Home
Index