---

Q = f== P ==  Q ==f== P  (e:{e:E| Q e} . e':{e:E| P e} . ((f e') = e))

---

Definitions :  and: P  Q,  weak-antecedent-function: Q ==f== P,  all: x:A. B[x],  exists: x:A. B[x],  set: {x:A| B[x]} ,  equal: s = t,  es-E: E,  apply: f a
FDL editor aliases :  weak-antecedent-surjection

---

Q  \mleftarrow{}\mleftarrow{}=  f==  P  ==    Q  \mleftarrow{}==f==  P  \mwedge{}  (\mforall{}e:\{e:E|  Q  e\}  .  \mexists{}e':\{e:E|  P  e\}  .  ((f  e')  =  e))


Date html generated: 2010_08_27-AM-09_39_18
Last ObjectModification: 2009_12_16-AM-08_53_31

Home Index