Nuprl Definition : bfs-predicate
bfs-predicate(K;S;p.P[p];b) == ∀p:|K| × S. (p ↓∈ b ⇒ P[p])
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
product: x:A × B[x],
rng_car: |r|,
bag-member: x ↓∈ bs
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs,
product: x:A × B[x],
rng_car: |r|
FDL editor aliases :
bfs-predicate
Latex:
bfs-predicate(K;S;p.P[p];b) == \mforall{}p:|K| \mtimes{} S. (p \mdownarrow{}\mmember{} b {}\mRightarrow{} P[p])
Date html generated:
2019_10_31-AM-06_28_20
Last ObjectModification:
2019_08_19-AM-10_42_31
Theory : linear!algebra
Home
Index