Nuprl Definition : fpf-compatible

|| ==  ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g)))  (f(x) g(x) ∈ B[x]))



Definitions occuring in Statement :  fpf-ap: f(x) fpf-dom: x ∈ dom(f) assert: b all: x:A. B[x] implies:  Q and: P ∧ Q equal: t ∈ T
Definitions occuring in definition :  all: x:A. B[x] implies:  Q and: P ∧ Q assert: b fpf-dom: x ∈ dom(f) equal: t ∈ T fpf-ap: f(x)
FDL editor aliases :  fpf-compatible

Latex:
f  ||  g  ==    \mforall{}x:A.  (((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}x  \mmember{}  dom(g)))  {}\mRightarrow{}  (f(x)  =  g(x)))



Date html generated: 2018_05_21-PM-09_19_50
Last ObjectModification: 2018_02_09-AM-10_17_44

Theory : finite!partial!functions


Home Index