Nuprl Definition : b_all
b_all(T;b;x.P[x]) == ∀x:T. (x ↓∈ b ⇒ P[x])
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs
FDL editor aliases :
b_all
Latex:
b\_all(T;b;x.P[x]) == \mforall{}x:T. (x \mdownarrow{}\mmember{} b {}\mRightarrow{} P[x])
Date html generated:
2016_05_15-PM-02_41_06
Last ObjectModification:
2015_09_23-AM-07_39_56
Theory : bags
Home
Index