Nuprl Definition : function-graph
function-graph{i:l}(A;a.B[a];grph) ==
(grph ⊆ Σa:A.B[a])
∧ (∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ grph)))))
∧ (∀a,b1,b2:coSet{i:l}.
((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ grph) ⇒ ((a,b2) ∈ grph) ⇒ seteq(b1;b2)))
Definitions occuring in Statement :
sigmaset: Σa:A.B[a],
setsubset: (a ⊆ b),
orderedpairset: (a,b),
setmem: (x ∈ s),
seteq: seteq(s1;s2),
coSet: coSet{i:l},
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
seteq: seteq(s1;s2),
orderedpairset: (a,b),
setmem: (x ∈ s),
implies: P ⇒ Q,
coSet: coSet{i:l},
all: ∀x:A. B[x],
and: P ∧ Q,
exists: ∃x:A. B[x],
sigmaset: Σa:A.B[a],
setsubset: (a ⊆ b)
FDL editor aliases :
function-graph
Latex:
function-graph\{i:l\}(A;a.B[a];grph) ==
(grph \msubseteq{} \mSigma{}a:A.B[a])
\mwedge{} (\mforall{}a:coSet\{i:l\}. ((a \mmember{} A) {}\mRightarrow{} (\mexists{}b:coSet\{i:l\}. ((b \mmember{} B[a]) \mwedge{} ((a,b) \mmember{} grph)))))
\mwedge{} (\mforall{}a,b1,b2:coSet\{i:l\}.
((a \mmember{} A)
{}\mRightarrow{} (b1 \mmember{} B[a])
{}\mRightarrow{} (b2 \mmember{} B[a])
{}\mRightarrow{} ((a,b1) \mmember{} grph)
{}\mRightarrow{} ((a,b2) \mmember{} grph)
{}\mRightarrow{} seteq(b1;b2)))
Date html generated:
2018_07_29-AM-10_05_12
Last ObjectModification:
2018_07_18-PM-04_38_35
Theory : constructive!set!theory
Home
Index