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