Nuprl Definition : regularset
A transitive set A is regular if for every set R that is a multi-valued
map from a member, B, to the whole set A, the range of the map R
is a set b in A. ⋅
regular(A) ==
transitive-set(A)
∧ (∀B:coSet{i:l}
((B ∈ A)
⇒ (∀R:coSet{i:l}
( setrel(R):(B ⇒ A) ⇒ (∃b:coSet{i:l}. ((b ∈ A) ∧ setrel(R):(B ⇒ b) ∧ setrel(R):(B ─>> b)))))))
Definitions occuring in Statement :
setrel: setrel(R),
onto-map: R:(A ─>> B),
mv-map: R:(A ⇒ B),
transitive-set: transitive-set(s),
setmem: (x ∈ s),
coSet: coSet{i:l},
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
setrel: setrel(R),
onto-map: R:(A ─>> B),
mv-map: R:(A ⇒ B),
and: P ∧ Q,
setmem: (x ∈ s),
coSet: coSet{i:l},
exists: ∃x:A. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
transitive-set: transitive-set(s)
FDL editor aliases :
regularset
Latex:
regular(A) ==
transitive-set(A)
\mwedge{} (\mforall{}B:coSet\{i:l\}
((B \mmember{} A)
{}\mRightarrow{} (\mforall{}R:coSet\{i:l\}
( setrel(R):(B {}\mRightarrow{} A)
{}\mRightarrow{} (\mexists{}b:coSet\{i:l\}. ((b \mmember{} A) \mwedge{} setrel(R):(B {}\mRightarrow{} b) \mwedge{} setrel(R):(B {}>> b)))))))
Date html generated:
2018_07_29-AM-10_06_39
Last ObjectModification:
2018_07_20-PM-01_28_02
Theory : constructive!set!theory
Home
Index