Nuprl Definition : fpf-compatible
f || g == ∀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: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
fpf-compatible
f || g == \mforall{}x:A. (((\muparrow{}x \mmember{} dom(f)) \mwedge{} (\muparrow{}x \mmember{} dom(g))) {}\mRightarrow{} (f(x) = g(x)))
Date html generated:
2015_07_17-AM-09_18_27
Last ObjectModification:
2012_02_25-AM-11_07_37
Home
Index