Nuprl Definition : fset-contains-none-of
fset-contains-none-of(eq;s;cs) ==  fset-null({c ∈ cs | deq-f-subset(eq) c s})
Definitions occuring in Statement : 
deq-f-subset: deq-f-subset(eq)
, 
fset-null: fset-null(s)
, 
fset-filter: {x ∈ s | P[x]}
, 
apply: f a
Definitions occuring in definition : 
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-contains-none-of
Latex:
fset-contains-none-of(eq;s;cs)  ==    fset-null(\{c  \mmember{}  cs  |  deq-f-subset(eq)  c  s\})
Date html generated:
2016_05_14-PM-03_42_03
Last ObjectModification:
2015_10_06-PM-11_51_30
Theory : finite!sets
Home
Index