Nuprl Definition : fset-ac-glb
fset-ac-glb(eq;ac1;ac2) ==
fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); f-union(deq-fset(eq);deq-fset(eq);ac1;as.λbs.as ⋃ bs"(ac2)))
Definitions occuring in Statement :
fset-minimals: fset-minimals(x,y.less[x; y]; s),
fset-image: f"(s),
f-proper-subset-dec: f-proper-subset-dec(eq;xs;ys),
deq-fset: deq-fset(eq),
f-union: f-union(domeq;rngeq;s;x.g[x]),
fset-union: x ⋃ y,
lambda: λx.A[x]
Definitions occuring in definition :
fset-minimals: fset-minimals(x,y.less[x; y]; s),
f-proper-subset-dec: f-proper-subset-dec(eq;xs;ys),
f-union: f-union(domeq;rngeq;s;x.g[x]),
fset-image: f"(s),
deq-fset: deq-fset(eq),
lambda: λx.A[x],
fset-union: x ⋃ y
FDL editor aliases :
fset-ac-glb
Latex:
fset-ac-glb(eq;ac1;ac2) ==
fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);
f-union(deq-fset(eq);deq-fset(eq);ac1;as.\mlambda{}bs.as \mcup{} bs"(ac2)))
Date html generated:
2016_05_14-PM-03_49_15
Last ObjectModification:
2015_10_06-PM-01_33_03
Theory : finite!sets
Home
Index