---

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)  (b1 = b2))))

---

Definitions :  assert: b,  fpf-dom: x  dom(f),  all: x:A. B[x],  l_member: (x  l),  fpf-ap: f(x),  implies: P  Q,  equal: s = 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: 2010_08_26-PM-11_45_00
Last ObjectModification: 2008_02_27-PM-09_37_51

Home Index