Nuprl Definition : f-proper-subset-dec
f-proper-subset-dec(eq;xs;ys) == (deq-f-subset(eq) xs ys) ∧b (¬b(deq-fset(eq) xs ys))
Definitions occuring in Statement :
deq-fset: deq-fset(eq),
deq-f-subset: deq-f-subset(eq),
band: p ∧b q,
bnot: ¬bb,
apply: f a
Definitions occuring in definition :
band: p ∧b q,
deq-f-subset: deq-f-subset(eq),
bnot: ¬bb,
apply: f a,
deq-fset: deq-fset(eq)
FDL editor aliases :
f-proper-subset-dec
Latex:
f-proper-subset-dec(eq;xs;ys) == (deq-f-subset(eq) xs ys) \mwedge{}\msubb{} (\mneg{}\msubb{}(deq-fset(eq) xs ys))
Date html generated:
2016_05_14-PM-03_41_53
Last ObjectModification:
2015_10_06-PM-01_36_07
Theory : finite!sets
Home
Index