Nuprl Definition : fpf-val
z != f(x) ==> P[a; z] ==  (↑x ∈ dom(f)) 
⇒ P[x; f(x)]
Definitions occuring in Statement : 
fpf-ap: f(x)
, 
fpf-dom: x ∈ dom(f)
, 
assert: ↑b
, 
implies: P 
⇒ Q
Definitions occuring in definition : 
implies: P 
⇒ Q
, 
assert: ↑b
, 
fpf-dom: x ∈ dom(f)
, 
fpf-ap: f(x)
FDL editor aliases : 
fpf-val
Latex:
z  !=  f(x)  ==>  P[a;  z]  ==    (\muparrow{}x  \mmember{}  dom(f))  {}\mRightarrow{}  P[x;  f(x)]
Date html generated:
2018_05_21-PM-09_18_33
Last ObjectModification:
2018_02_09-AM-10_17_11
Theory : finite!partial!functions
Home
Index