Nuprl Definition : singlevalued-graph
singlevalued-graph(A;a.B[a];grph) == ∀a∈A.∀b1∈B[a].∀b2∈B[a].((a,b1) ∈ grph) ⇒ ((a,b2) ∈ grph) ⇒ seteq(b1;b2)
Definitions occuring in Statement :
allsetmem: ∀a∈A.P[a],
orderedpairset: (a,b),
setmem: (x ∈ s),
seteq: seteq(s1;s2),
implies: P ⇒ Q
Definitions occuring in definition :
seteq: seteq(s1;s2),
orderedpairset: (a,b),
setmem: (x ∈ s),
implies: P ⇒ Q,
allsetmem: ∀a∈A.P[a]
FDL editor aliases :
singlevalued-graph
Latex:
singlevalued-graph(A;a.B[a];grph) ==
\mforall{}a\mmember{}A.\mforall{}b1\mmember{}B[a].\mforall{}b2\mmember{}B[a].((a,b1) \mmember{} grph) {}\mRightarrow{} ((a,b2) \mmember{} grph) {}\mRightarrow{} seteq(b1;b2)
Date html generated:
2018_05_29-PM-01_50_31
Last ObjectModification:
2018_05_26-PM-07_46_42
Theory : constructive!set!theory
Home
Index