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
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
assert: ↑b,
fpf-dom: x ∈ dom(f),
equal: s = 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