Nuprl Definition : fun-equiv

fun-equiv(X;a,b.E[a; b];f;g) ==  ∀x:X. E[f x; g x]


Definitions occuring in Statement :  all: ∀x:A. B[x],  apply: f a
Definitions occuring in definition :  all: ∀x:A. B[x],  apply: f a
FDL editor aliases :  fun-equiv
Latex:
fun-equiv(X;a,b.E[a;  b];f;g)  ==    \mforall{}x:X.  E[f  x;  g  x]


Date html generated: 2016_05_14-AM-06_09_06
Last ObjectModification: 2015_09_22-PM-05_46_13

Theory : quot_1


Home Index