Nuprl Definition : deq-disjoint
deq-disjoint(eq;as;bs) == (∀a∈as.¬ba ∈b bs)_b
Definitions occuring in Statement :
bl-all: (∀x∈L.P[x])_b,
deq-member: x ∈b L,
bnot: ¬bb
Definitions occuring in definition :
bl-all: (∀x∈L.P[x])_b,
bnot: ¬bb,
deq-member: x ∈b L
FDL editor aliases :
deq-disjoint
Latex:
deq-disjoint(eq;as;bs) == (\mforall{}a\mmember{}as.\mneg{}\msubb{}a \mmember{}\msubb{} bs)\_b
Date html generated:
2016_05_14-PM-03_23_59
Last ObjectModification:
2015_09_22-PM-05_59_31
Theory : decidable!equality
Home
Index