Nuprl Definition : bounded-relation
Bounded(x,a.R[x; a]) ==
(∀x1,x2,a1,a2:Set{i:l}. (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ R[x1; a1] ⇒ R[x2; a2]))
∧ (∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x; a] ⇐⇒ (a ∈ y)))
∧ (∃B:Set{i:l}. ∀x,a:Set{i:l}. (R[x; a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
Definitions occuring in Statement :
setimage: setimage{i:l}(x;b),
setmem: (x ∈ s),
seteq: seteq(s1;s2),
Set: Set{i:l},
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
setimage: setimage{i:l}(x;b),
setmem: (x ∈ s),
and: P ∧ Q,
Set: Set{i:l},
exists: ∃x:A. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
seteq: seteq(s1;s2)
FDL editor aliases :
bounded-relation
Latex:
Bounded(x,a.R[x; a]) ==
(\mforall{}x1,x2,a1,a2:Set\{i:l\}. (seteq(x1;x2) {}\mRightarrow{} seteq(a1;a2) {}\mRightarrow{} R[x1; a1] {}\mRightarrow{} R[x2; a2]))
\mwedge{} (\mforall{}x:Set\{i:l\}. \mexists{}y:Set\{i:l\}. \mforall{}a:Set\{i:l\}. (R[x; a] \mLeftarrow{}{}\mRightarrow{} (a \mmember{} y)))
\mwedge{} (\mexists{}B:Set\{i:l\}. \mforall{}x,a:Set\{i:l\}. (R[x; a] {}\mRightarrow{} (\mexists{}b:Set\{i:l\}. ((b \mmember{} B) \mwedge{} setimage\{i:l\}(x;b)))))
Date html generated:
2018_05_29-PM-01_54_13
Last ObjectModification:
2018_05_29-AM-11_28_07
Theory : constructive!set!theory
Home
Index