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
Definitions occuring in definition :  all: ∀x:A. B[x],  and: P ∧ Q,  fpf-dom: x ∈ dom(f),  implies: P ⇒ Q,  not: ¬A,  assert: ↑b,  apply: f a,  equal: s = t ∈ T,  fpf-ap: f(x)
FDL editor aliases :  fpf-compatible-mod
Latex:
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: 2018_05_21-PM-09_20_03
Last ObjectModification: 2018_02_09-AM-10_17_50

Theory : finite!partial!functions


Home Index