Nuprl Definition : bag-incomparable
bag-incomparable(T;R;b) == ∀x,y:T. (x ↓∈ b ⇒ y ↓∈ b ⇒ (¬(x R y)))
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
infix_ap: x f y,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs,
not: ¬A,
infix_ap: x f y
FDL editor aliases :
bag-incomparable
Latex:
bag-incomparable(T;R;b) == \mforall{}x,y:T. (x \mdownarrow{}\mmember{} b {}\mRightarrow{} y \mdownarrow{}\mmember{} b {}\mRightarrow{} (\mneg{}(x R y)))
Date html generated:
2016_05_15-PM-03_12_04
Last ObjectModification:
2015_09_23-AM-07_42_25
Theory : bags
Home
Index