Nuprl Definition : fset-ac-le
fset-ac-le(eq;ac1;ac2) == fset-all(ac1;x.¬bfset-null({y ∈ ac2 | deq-f-subset(eq) y x}))
Definitions occuring in Statement :
deq-f-subset: deq-f-subset(eq),
fset-all: fset-all(s;x.P[x]),
fset-null: fset-null(s),
fset-filter: {x ∈ s | P[x]},
bnot: ¬bb,
apply: f a
Definitions occuring in definition :
fset-all: fset-all(s;x.P[x]),
bnot: ¬bb,
fset-null: fset-null(s),
fset-filter: {x ∈ s | P[x]},
apply: f a,
deq-f-subset: deq-f-subset(eq)
FDL editor aliases :
fset-ac-le
Latex:
fset-ac-le(eq;ac1;ac2) == fset-all(ac1;x.\mneg{}\msubb{}fset-null(\{y \mmember{} ac2 | deq-f-subset(eq) y x\}))
Date html generated:
2016_05_14-PM-03_42_58
Last ObjectModification:
2015_10_06-PM-01_35_48
Theory : finite!sets
Home
Index