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