Nuprl Definition : fset-constrained-ac-glb
glb(P;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) s.t. P))
Definitions occuring in Statement :
fset-minimals: fset-minimals(x,y.less[x; y]; s),
fset-constrained-image: f"(s) s.t. P,
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-constrained-image: f"(s) s.t. P,
deq-fset: deq-fset(eq),
lambda: λx.A[x],
fset-union: x ⋃ y
FDL editor aliases :
fset-constrained-ac-glb
Latex:
glb(P;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) s.t. P))
Date html generated:
2016_05_14-PM-03_49_59
Last ObjectModification:
2015_10_06-PM-01_32_51
Theory : finite!sets
Home
Index