Nuprl Definition : bar-equal

bar-equal(T;x;y) ==  ∀a:T. (x↓a ⇐⇒ y↓a)


Definitions occuring in Statement :  bar-converges: x↓a,  all: ∀x:A. B[x],  iff: P ⇐⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  bar-converges: x↓a
FDL editor aliases :  bar-equal
Latex:
bar-equal(T;x;y)  ==    \mforall{}a:T.  (x\mdownarrow{}a  \mLeftarrow{}{}\mRightarrow{}  y\mdownarrow{}a)


Date html generated: 2016_05_14-AM-06_20_27
Last ObjectModification: 2015_09_22-PM-05_47_41

Theory : co-recursion


Home Index