Nuprl Definition : least-closed-set

By iterating over all the members of a regular set containg the transitive
closure of set B we can form the least set closed under function G,
provided that B is a bound for G in a suitable sense.
(Spelled out in the lemma Error :least-closed-set-inductively-defined).⋅

least-closed-set(B;G) == ⋃a∈regext(setTC(B)).itersetfun(x.G x;a)

Definitions occuring in Statement : regext: regext(a), itersetfun: itersetfun(s.G[s];a), setTC: setTC(a), setunionfun: ⋃x∈s.f[x], apply: f a
Definitions occuring in definition : setunionfun: ⋃x∈s.f[x], itersetfun: itersetfun(s.G[s];a), apply: f a, regext: regext(a), setTC: Error :setTC
FDL editor aliases : least-closed-set

Latex:
least-closed-set(B;G) == \mcup{}a\mmember{}regext(setTC(B)).itersetfun(x.G x;a) Date html generated: 2018_07_29-AM-10_09_38 Last ObjectModification: 2018_05_30-PM-07_02_38 Theory : constructive!set!theory Home Index