Nuprl Definition : bag-covers
bag-covers(T;R;cvr;b) ==  ∀x:T. (x ↓∈ b 
⇒ (x ↓∈ cvr ∨ (∃y:T. (y ↓∈ cvr ∧ (x R y)))))
Definitions occuring in Statement : 
bag-member: x ↓∈ bs
, 
infix_ap: x f y
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
bag-member: x ↓∈ bs
, 
infix_ap: x f y
FDL editor aliases : 
bag-covers
Latex:
bag-covers(T;R;cvr;b)  ==    \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (x  \mdownarrow{}\mmember{}  cvr  \mvee{}  (\mexists{}y:T.  (y  \mdownarrow{}\mmember{}  cvr  \mwedge{}  (x  R  y)))))
Date html generated:
2016_05_15-PM-03_12_17
Last ObjectModification:
2015_09_23-AM-07_42_30
Theory : bags
Home
Index