Nuprl Definition : free-dlwc-inc
free-dlwc-inc(eq;a.Cs[a];x) == if fset-null({c ∈ Cs[x] | deq-f-subset(eq) c {x}}) then {{x}} else {} fi
Definitions occuring in Statement :
deq-f-subset: deq-f-subset(eq),
empty-fset: {},
fset-null: fset-null(s),
fset-filter: {x ∈ s | P[x]},
fset-singleton: {x},
ifthenelse: if b then t else f fi ,
apply: f a
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
fset-null: fset-null(s),
fset-filter: {x ∈ s | P[x]},
apply: f a,
deq-f-subset: deq-f-subset(eq),
fset-singleton: {x},
empty-fset: {}
FDL editor aliases :
free-dlwc-inc
Latex:
free-dlwc-inc(eq;a.Cs[a];x) ==
if fset-null(\{c \mmember{} Cs[x] | deq-f-subset(eq) c \{x\}\}) then \{\{x\}\} else \{\} fi
Date html generated:
2020_05_20-AM-08_48_38
Last ObjectModification:
2015_10_08-AM-10_46_36
Theory : lattices
Home
Index