Nuprl Definition : binrel_eqv
E <≡>{T} E' == ∀x,y:T. (E x y ⇐⇒ E' x y)
Definitions occuring in Statement :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a
Latex:
E <\mequiv{}>\{T\} E' == \mforall{}x,y:T. (E x y \mLeftarrow{}{}\mRightarrow{} E' x y)
Date html generated:
2016_05_14-PM-03_54_36
Last ObjectModification:
2015_09_22-PM-06_01_49
Theory : relations2
Home
Index