x
dom(f). v=f(x) 
P[x; v] == x:A. ((
x dom(f)) P[x; f(x)])
Definitions :
all: x:A. B[x],
implies: P Q,
assert: b,
fpf-dom: x dom(f),
fpf-ap: f(x)
FDL editor aliases :
fpf-all
\mforall{}x\mmember{}dom(f). v=f(x) {}\mRightarrow{} P[x; v] == \mforall{}x:A. ((\muparrow{}x \mmember{} dom(f)) {}\mRightarrow{} P[x; f(x)])
Date html generated:
2010_08_26-PM-11_58_08
Last ObjectModification:
2008_02_27-PM-09_43_31
Home
Index