Nuprl Definition : fpf-single-valued
fpf-single-valued(A;eq;x.B[x];V;g) ==
∀x:A. ((↑x ∈ dom(g)) ⇒ (∀b1,b2:B[x]. ((b1 ∈ g(x)) ⇒ (b2 ∈ g(x)) ⇒ (b1 = b2 ∈ V) ⇒ (b1 = b2 ∈ B[x]))))
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
l_member: (x ∈ l),
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
assert: ↑b,
fpf-dom: x ∈ dom(f),
all: ∀x:A. B[x],
l_member: (x ∈ l),
fpf-ap: f(x),
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
fpf-single-valued
Latex:
fpf-single-valued(A;eq;x.B[x];V;g) ==
\mforall{}x:A. ((\muparrow{}x \mmember{} dom(g)) {}\mRightarrow{} (\mforall{}b1,b2:B[x]. ((b1 \mmember{} g(x)) {}\mRightarrow{} (b2 \mmember{} g(x)) {}\mRightarrow{} (b1 = b2) {}\mRightarrow{} (b1 = b2))))
Date html generated:
2018_05_21-PM-09_18_25
Last ObjectModification:
2018_02_09-AM-10_17_08
Theory : finite!partial!functions
Home
Index