Nuprl Definition : fset-closed
(s closed under fs) ==  (∀f∈fs.∀x:T. f x ∈ s supposing x ∈ s)
Definitions occuring in Statement : 
fset-member: a ∈ s
, 
l_all: (∀x∈L.P[x])
, 
uimplies: b supposing a
, 
all: ∀x:A. B[x]
, 
apply: f a
Definitions occuring in definition : 
l_all: (∀x∈L.P[x])
, 
all: ∀x:A. B[x]
, 
uimplies: b supposing a
, 
fset-member: a ∈ s
, 
apply: f a
FDL editor aliases : 
fset-closed
Latex:
(s  closed  under  fs)  ==    (\mforall{}f\mmember{}fs.\mforall{}x:T.  f  x  \mmember{}  s  supposing  x  \mmember{}  s)
Date html generated:
2016_05_14-PM-03_44_37
Last ObjectModification:
2015_10_06-PM-01_35_01
Theory : finite!sets
Home
Index