Nuprl Definition : fpf-single-valued

fpf-single-valued(A;eq;x.B[x];V;g) ==
  ∀x:A. ((↑x ∈ dom(g))  (∀b1,b2:B[x].  ((b1 ∈ g(x))  (b2 ∈ g(x))  (b1 b2 ∈ V)  (b1 b2 ∈ B[x]))))



Definitions occuring in Statement :  fpf-ap: f(x) fpf-dom: x ∈ dom(f) l_member: (x ∈ l) assert: b all: x:A. B[x] implies:  Q equal: t ∈ T
FDL editor aliases :  fpf-single-valued
fpf-single-valued(A;eq;x.B[x];V;g)  ==
    \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(g))  {}\mRightarrow{}  (\mforall{}b1,b2:B[x].    ((b1  \mmember{}  g(x))  {}\mRightarrow{}  (b2  \mmember{}  g(x))  {}\mRightarrow{}  (b1  =  b2)  {}\mRightarrow{}  (b1  =  b2))))



Date html generated: 2015_07_17-AM-09_16_54
Last ObjectModification: 2012_02_25-AM-11_06_39

Home Index