Nuprl Definition : fun-sep

fun-sep(ss;A;f;g) ==  ∃a:A. f a # g a


Definitions occuring in Statement :  ss-sep: x # y,  exists: ∃x:A. B[x],  apply: f a
Definitions occuring in definition :  exists: ∃x:A. B[x],  ss-sep: x # y,  apply: f a
FDL editor aliases :  fun-sep
Latex:
fun-sep(ss;A;f;g)  ==    \mexists{}a:A.  f  a  \#  g  a


Date html generated: 2019_10_31-AM-07_26_35
Last ObjectModification: 2019_03_19-PM-03_41_15

Theory : constructive!algebra


Home Index