Nuprl Definition : fpf-compatible-mod
fpf-compatible-mod(A;a.B[a];eq;
R;f;g) ==
∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (¬↑(R f(x) g(x))) ⇒ (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],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
fpf-compatible-mod
fpf-compatible-mod(A;a.B[a];eq;
R;f;g) ==
\mforall{}x:A. (((\muparrow{}x \mmember{} dom(f)) \mwedge{} (\muparrow{}x \mmember{} dom(g))) {}\mRightarrow{} (\mneg{}\muparrow{}(R f(x) g(x))) {}\mRightarrow{} (f(x) = g(x)))
Date html generated:
2015_07_17-AM-09_18_37
Last ObjectModification:
2012_02_25-AM-11_07_46
Home
Index