Nuprl Definition : fset-antichain
fset-antichain(eq;ac) == fset-pairwise(xs,ys.¬bf-proper-subset-dec(eq;xs;ys);ac)
Definitions occuring in Statement :
fset-pairwise: fset-pairwise(x,y.R[x; y];s),
f-proper-subset-dec: f-proper-subset-dec(eq;xs;ys),
bnot: ¬bb
Definitions occuring in definition :
fset-pairwise: fset-pairwise(x,y.R[x; y];s),
bnot: ¬bb,
f-proper-subset-dec: f-proper-subset-dec(eq;xs;ys)
FDL editor aliases :
fset-antichain
Latex:
fset-antichain(eq;ac) == fset-pairwise(xs,ys.\mneg{}\msubb{}f-proper-subset-dec(eq;xs;ys);ac)
Date html generated:
2016_05_14-PM-03_42_36
Last ObjectModification:
2015_10_06-PM-01_35_55
Theory : finite!sets
Home
Index