Nuprl Definition : Regularcoset
cRegular(A) ==
transitive-set(A)
∧ (∀B:coSet{i:l}
((B ∈ A)
⇒ (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
(coSetRelation(R) ⇒ R:(B ⇒ A) ⇒ (∃b:coSet{i:l}. ((b ∈ A) ∧ R:(B ⇒ b) ∧ R:(B ─>> b)))))))
Definitions occuring in Statement :
onto-map: R:(A ─>> B),
mv-map: R:(A ⇒ B),
coset-relation: coSetRelation(R),
transitive-set: transitive-set(s),
setmem: (x ∈ s),
coSet: coSet{i:l},
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
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,
coset-relation: coSetRelation(R),
prop: ℙ,
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
transitive-set: transitive-set(s)
FDL editor aliases :
Regularcoset
Latex:
cRegular(A) ==
transitive-set(A)
\mwedge{} (\mforall{}B:coSet\{i:l\}
((B \mmember{} A)
{}\mRightarrow{} (\mforall{}R:coSet\{i:l\} {}\mrightarrow{} coSet\{i:l\} {}\mrightarrow{} \mBbbP{}'
(coSetRelation(R)
{}\mRightarrow{} R:(B {}\mRightarrow{} A)
{}\mRightarrow{} (\mexists{}b:coSet\{i:l\}. ((b \mmember{} A) \mwedge{} R:(B {}\mRightarrow{} b) \mwedge{} R:(B {}>> b)))))))
Date html generated:
2018_07_29-AM-10_06_46
Last ObjectModification:
2018_07_20-PM-01_35_28
Theory : constructive!set!theory
Home
Index